> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.
I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.
The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.
The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.
For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?
The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.
Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
loading story #50204692
loading story #50204500
loading story #50204482
You can see that the blog post does not claim to solve the halting problem; instead, they pick a subset of behavior that is likely to be useful.
loading story #50218114