I'm reminded of this apocryphal story of a revered machinist from Tampere. The city is on an isthmus between two lakes. Their shop was right next to the rapids between the lakes. They were famous, having never made any mistakes.

During some construction event, the city closed off the rapids and no water was flowing there, it was completely dry. There was a massive amount of partially machined objects on the bottom. The machinist had been tossing them out of the window into the water, every time when they made a mistake.

So the machinist had been using rigorous testing, catching all defects prior to release, rather than using a correct-by-construction methodology. Either approach seems fine.

Neither is perfect. Tests are only as good as your imagination of what to test. Proof by construction is only as good as your ability to have the right axioms

> Tests are only as good as your imagination of what to test.

A lot of work has been done on code-coverage, boundary-analysis, etc. Testing can never be complete, though.

> Proof by construction is only as good as your ability to have the right axioms

That's not a good summary of the challenges that formal methods face with respect to correctness. Defects can creep in at various points.

See p. 46 of the PDF linked from https://www.adacore.com/tokeneer

Well, apparently it didn’t catch the defect that mattered. Typical engineer trying to justify an engineering mistake!

He never had problem with use-after-free, because he was leaking memory.