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.
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.