[jmalicki]

The other huge thing a ton of people miss when repeating is that the undecidability is between "definitely terminates" vs. "definitely does not terminate".

A ton of useful stuff (for instance in compiler optimizers) can be done with deciding between "trivial to prove it terminates" vs. "who knows, this instance of the problem is hard! I'll just skip this optimization in this ridiculously non-representatively rare case."