[WCSTombs]

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.

[user1138]

You're correct on the citations though that will probably be very easy as we have many people claiming exactly that. As to your second point, yes, and the safety claims being made are not restricted to those decidable subsets. The moment you claim general safety guarantees for systems operating beyond those constrained subsets you're back in full Rice territory. If you can name a total language with an early termination guarantee, I'm all ears. You asked for my citations, now show me yours.

[user1138]

While I do have a formal citations there is this https://venturebeat.com/ai/lean4-how-the-theorem-prover-work...

[WCSTombs]

Not only is this just a random article from the internet, as opposed to something peer-reviewed, but more importantly, nowhere does it even attempt to claim that the mere fact of a program terminating implies its suitability in a safety context.