alt Hacker News> 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."