The point is that it can get really, really hard for a static analyzer to be complete if you ask for enough generality in your static analyzer.
The proof basically works by showing that if you figured out a way to say, automatically find bugs in programs and making sure the program meets the specification, or figuring out whether a program actually is platonically implementing the square function infallibly, or any other program that identifies non-trivial, semantic properties, we could convert it into a program that solves the halting problem, and thus the program must be at least be able to solve all recursively enumerable problems.
For a more in practice example of static analysis being hard, I’d say a lot of NP and Co-NP completeness results of lots of problems, or even PSPACE-completeness for problems like model checking show that unless huge assumptions are made about physics, completeness of static analysis is a pipe dream for even limited areas.
Static analysis will likely be very hard for a long time to come.
My objection is to “IRL” and “in practice” in your top level comment, as if this is what static analysis is actually concerned with. In various formal questions, halting problem is a big deal, and I expect the same shape to be important in decision theory of the future (which might be an invention that humans will be too late to be first to develop). Being cooperative about loops of mutual prediction seems crucial for (acausal) coordination, the halting problem just observes that the same ingredients can be used to destroy all possibility of coordination.
The point is that it can get really, really hard for a static analyzer to be complete if you ask for enough generality in your static analyzer.
The proof basically works by showing that if you figured out a way to say, automatically find bugs in programs and making sure the program meets the specification, or figuring out whether a program actually is platonically implementing the square function infallibly, or any other program that identifies non-trivial, semantic properties, we could convert it into a program that solves the halting problem, and thus the program must be at least be able to solve all recursively enumerable problems.
For a more in practice example of static analysis being hard, I’d say a lot of NP and Co-NP completeness results of lots of problems, or even PSPACE-completeness for problems like model checking show that unless huge assumptions are made about physics, completeness of static analysis is a pipe dream for even limited areas.
Static analysis will likely be very hard for a long time to come.
My objection is to “IRL” and “in practice” in your top level comment, as if this is what static analysis is actually concerned with. In various formal questions, halting problem is a big deal, and I expect the same shape to be important in decision theory of the future (which might be an invention that humans will be too late to be first to develop). Being cooperative about loops of mutual prediction seems crucial for (acausal) coordination, the halting problem just observes that the same ingredients can be used to destroy all possibility of coordination.