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.
You can't formally verify code when the code hasn't even met the spec yet! It takes a huge amount of time and effort to achieve this! Even when you think you've achieved this and your code meets the spec word-for-word, some stakeholders will still disagree based on technicalities and definitions!
How in the world are we supposed to prove that code is correct when people can't even agree on the same definition of 'correct'?! That's most of the work, really.
Also, if it takes people 1 year to complete a project in such a way that it barely just meets the spec to an acceptable standard, and only in a pure high level business sense; just barely covering all the basic exception handling scenarios; how long is it going to take to add formal verification on top of that? How many more gaps will have to be plugged, how many more assumptions will need to be enumerated, in order to make your formal proof air-tight? Then what happens if the client reads your formal proof and informs you that some of your assumptions are incorrect? What value is your proof then?