I do acknowledge this. My point is that turing-completeness is not necessarily a desirable aspect of a language. You can check out Agda if you are interested in what can be done with a total language.

For some use-cases, like seting up a mainloop, you need an escape hatch because that mainloop is not going to be total. But not every program needs that. Conversely, a programming language that doesn't care about totality won't be able to sere other use-cases, such as building proven programs. My understanding is that it's much easier to build an escape hatch in total languages, than it is to retrofit non-total languages to prove programs.