Formally verifying Advent of Code using Dijkstra's program construction(haripm.com)
haripm.com
Formally verifying Advent of Code using Dijkstra's program construction
https://haripm.com/blog/aoc-day-3-without-thinking/
8 comments
That's a lot of manual effort to save just a tiny bit of thinking. The first digit is the largest digit among the first N-1 digits. The second digit is the largest digit to the right of the first digit up to and including the Nth digit. That's it.
Hi! Yes, I talk about this a little bit at the end and I solve Part 2 the normal way. This is a toy example that I did for fun. The objective was to introduce people to Program Construction and show how you can use formal methods to derive correct programs. Whether the juice is worth the squeeze is a judgement call that you make depending on how critical the software you are writing is.
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.
To me it seems more like a lot of _thinking_ just to save a tiny bit of thinking.
It was a fun read though, and obviously this exercise is not about efficiency so much as exploring an interesting idea.
It was a fun read though, and obviously this exercise is not about efficiency so much as exploring an interesting idea.
Maybe you missed this part: “That seemed like a lot of thinking, you might object. It probably was if you’re not familiar with Program Construction yet, but once you’ve derived a couple of these theorems, you’ll find that there is no thinking involved. Not in the sense that once you’re good at something, you can do it almost mechanically, but in the sense that there’s only one way this could have gone. Starting from that post-condition, the theorems we proved fall out automatically as we continue expanding our model, and the same can be said for our loop body. Program construction is really easy in that way, because all you’re doing is following the program derivation to its logical
end.”
The benefit of that effort is that you know the program is provably correct.
I was drilled in using the GCL (and variations on it) in Eindhoven TUE and Amsterdam UvA a long time ago, nice to see it here. Not very practical these days but good for brain.
Wow, this is certainly a new perspective for solving this problem