Sometimes I wonder whether Silicon Valley programmers take this kind of difficult programming as a given. I tend to think in terms of simple programs, and while formal verification isn't bad, I question whether that's really software development.

I know that in the AI era, with code being generated in enormous quantities, formal verification is important. It is effective to some degree, but in my view, software that requires provable correctness is only a subset of all software, and I agree with the author that a kind of empiricism is the right approach. Because most of it is based on understanding a customer's "requirements." And if we consider that not all requirements can be formally proven mathematically, then in practice the line between where formal verification is used and where it isn't will become clearly drawn.

Formal specification is the work of deciding where the target is, and formal verification is the work of hitting that target with an arrow. But most of software development is the work of deciding where the target ought to be. Formal specification is like shooting an arrow at a moving target and hitting the bullseye, but figuring out where to pin that target down is software development, and honestly, most of software development spends more time pinning the target's position. Especially in the AI era, even more so.