Skip to content

Comment on Formally verifying Advent of Code using Dijkstra's program constructionparent

Comments

But the resulting algorithm is just... weird. It operates under the assumption that the elements f.i can be arbitrary e.g. negative or greater than 9 — which they can't. And adopting that assumption allows you to dispense with keeping track of the variations of the total sum and merely track the separate digits themselves, which would allow a non-mechanical programmer to see easily that the algorithm is correct.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.