The formal verification and AI safety literature frequently cite total languages as a solution to the halting problem. This paper argues that this claim relies on a binary reduction of a trinary problem. While total languages provide an exit proof (halting), they cannot provide a correct-exit proof without step-by-step verification, which is itself the halting problem.

Using Rice’s Theorem (1953) and Turing’s second proof (1936), I demonstrate that "early termination"—halting at an unintended point with incorrect output—is a non-trivial semantic property and therefore undecidable. The safety guarantees currently being marketed are often just tautologies where "termination" has been swapped for "safety".

No novel math here—just a careful reading of the foundational proofs we’ve had for decades.

First, who is saying "termination implies safety"? There need to be a citations for that, so we can know what specific claim is supposedly being refuted here.

Second, Rice's theorem states that no nontrivial property on the set of partial recursive functions is decidable. However, there are subsets of the set of all recursive functions that do have decidable properties, and it's pretty trivial to cook some of them up. Since some of these sub-languages also consist only of total functions, there are "total languages" for which the analogous statement of Rice's theorem is false. To fix this we would need to choose a specific total language. There could be some interesting ones for which the analogous statement of Rice's theorem still holds, but I'm not an expert on that.