This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Those provide formal verification of some aspects of the code. And that's great! It's progress!
Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation that "it's amazing how many bugs there can be in a formally verified program" is no longer true.)
> This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools".
Well, in AI, the process is called "AI can never succeed". So maybe the general thing is "X can never succeed", where X is some hugely ambitious (and ambiguous) thing, like "AI" or "formal software verification" or "curing cancer".
We're probably never going to cure cancer - that is, have some treatment that conquers all cancers. Instead, we get "for this specific type of cancer, for these specific conditions, this treatment has a higher survival rate than the ones we had before". Over time, that adds up to a lot of people living out their days rather than dying early.
And maybe software verification is the same. Enough ways of verifying specific aspects of software, and bugs have fewer places to hide. It won't find all bugs, but we'll still get better software.
But "X can never succeed" isn't a very catchy phrase. Can anyone coin a better one? (Or, is there already a better one that I don't know about?)
Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation that "it's amazing how many bugs there can be in a formally verified program" is no longer true.)