> 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 properties hold across those models.
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 normal and 10x as long it’s not real world useable today.
> If the smartest engineers cannot do it, it doesn’t work.
[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.
> 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.
The problem is, it’s unclear exactly what those situations are or even should be. That lack of clarity causes us to fail to recognize when we could have applied these methods and so we just don’t. As much as I see value in formal methods, I’ve never worked with a team that has employed them. And I don’t think I’m at all unique in that.
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 properties hold across those models.