[annywhey]

I think the devil is in the details of this one.

The shop coder may have never heard of a formal method and thinks it is something that must be "slow" or "too complicated", but they inevitably come crashing into tools and techniques that were informed by formal methods. In the 80's it was hard to get your hands on a C compiler. In the 90's, everyone still thought that OOP was going to change everything. By the 00's we finally saw widespread adoption of garbage collected languages. And more recently we've had better package management and efforts to rework lower level coding.

We've never left behind cargo-culting, given the growth in the number of programmers, but the strides are there, always hovering a few steps behind the code that is considered the "production code". The production code is seen as far too fast moving to be considered for "formal methods", yet it still ends up using "design patterns", echoing Hoare's notes about defensive coding techniques. We don't "prove" our C++ code is good, but we run a "static analysis" tool or a "fuzzer" on it.

Perfect, the enemy of good enough.

[repolfx]

Sure, but if you look carefully most static analysis engines are developed by industry not academia because they're collections of heuristics that tend to work in practice rather than lots of clever-as-possible sounding theory.

But Hoare talks specifically about formal methods, which is widely understood to mean proving code meets a spec using techniques like constraint solvers. Dependent types may meet the definition too. And none of these techniques are used widely or have ever been used widely.