Earlier quoted context omitted.
> If formal verification hinges on having perfect engineers then it’s useless because perfect engineers wouldn’t need formal verification. It doesn’t hinge on having perfect engineers. It hinges on engineers being able to model problems algebraically and completely, prove the equivalence of multiple such models at different layers of abstraction (including equivalence to the original code), and then prove that useful…
If the smartest engineers cannot do it, it doesn’t work. This isn’t even getting to the practical question of whether it’s worth doing, given the significant additional cost. If the smartest folks you can find are not smart enough to use the framework then it’s useless. Maybe this means the tooling is insufficient. Maybe it means the field isn’t mature enough. Whatever, if you need an IQ two standard deviations above…
[FIX:] ..., it doesn't work universally.
And the answer to that is pretty clear. It does not work universally. If every developer started only shipping code they had credibly formally verified, the vast majority of developers would go into shock at the scale of work to be done. Even the best "validators" would fall into career shredding pits, due to "minor" but now insurmountable dependencies in previously unverified projects. The vast majority of projects would go into unrecoverable stalls.
But formal validation can still work some of the time with the right people, on the right scale and kind of project, with the right amount of resources/time expended.
It isn't as if regular "best practices" programming works universally either. But validation is much harder.