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.

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