Do you have any reason to believe that all the rest of the verification theory is completely impractical when every piece that was packaged in a usable context became a hit?
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.)
Yes indeed. That is insightful.
Is there a name for this process?
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?)
I have no reason why any of them could not be successful. I don't expect all of them to be, but anyone that gets there is already a huge advance.
While I am by no means have enough knowledge to claim such, but let’s just add that ordinary types are a so-called “trivial property”. Many, actually interesting properties can’t be proved as per Rice’s theorem in every case.
This tool does the former, leaving the latter up to humans.