I think it’s worth noting that Rice’s theorem and the undecidability of the halting problem apply to arbitrary programs. In practice, the programs that humans w

I think it’s worth noting that Rice’s theorem and the undecidability of the halting problem apply to arbitrary programs. In practice, the programs that humans write are very much non-arbitrary. Moreover, sometimes we’re happy to trade a bit of expressive power in exchange for stronger guarantees—like using a total/strongly-normalising language in which the answer to “Does this program terminate for all inputs?” is always “Yes”. In a similar vein, most real numbers are uncomputable, but we pretty much only care about the computable ones AFAIK.