> not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth...

We ought to be able to build high-confidence software.

Unless you have bamboozled your customers completely, they should expect a product that you provide to be a) fit for purpose, b) fit for use, and c) secure.

We know of course that very little commercial software is (d) proven correct. Software Correctness (d) is hard, no question.

Just getting to ONE of { a, b, c } appears to be a bridge too far. But that's where professional rigour and diligence is required.

btw good article, u/turbobutton.