[MaxBarraclough]

I don't think anyone is going to dispute that though, except perhaps on a point of detail: it took Hoare logic to bridge the gap between imperative programming and 'ordinary' mathematical logic.

If I'm reading them right, urthor's point is that the average programmer doesn't directly benefit from being skilled in developing formal proofs about code. (I rambled at some length on this topic recently. [0]) Very few software development workplaces value correctness so highly that they invest in formal methods.

That said, I think the case can be made that learning about formal methods is useful in instilling a sense of how rigorous software development can be, and perhaps to develop a healthy contempt for hand-wavy sloppiness. Perhaps it's also helpful to learn that informal requirements, formal specifications, and implementations, are three different things. I think this may be true even if we rarely use formal specifications in practice.

[0] https://news.ycombinator.com/item?id=30000146