[amackera]

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.

[layer8]

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.”