First, no rescue is needed. I said that not tracking complexity is a matter of choice, and you mistakenly thought it amounts to deciding halting; I pointed out the well-known fact that it isn't. Second, you don't need a non-Turing-complete language in order to track computational complexity in the type system, just as you don't need a language that cannot perform IO in order to track IO in the type system.

As to JavaScript, there are much more commonplace things that it doesn't track in the type system, either, and they're all a matter of choice. There is no theory that says what should or shouldn't be tracked, and no definitive empirical results that can settle all those questions, either. At the end of the day, what you choose to track is a matter of preference.

> I said that not tracking complexity is a matter of choice, and you mistakenly thought it amounts to deciding halting

And you implicitly acknowledged this fact by using TPL as example: you know, the class of language where all you can write is a provably halting program (that's the definition of Total programming languages!).

The halting problem being a property of Turing-complete languages, you just sidestepped the issue here.

You can track complexity in Turing complete languages, just as you can track effects; neither should bother you more than the other. While doing either precisely amounts to deciding halting, the way it is done in programming languages does not (when we track effects the type system does not tell us an effect will occur, only that it may; similarly for complexity -- we track the worst-case complexity of a given term, which, for Turing complete languages, can be infinite for some terms, but certainly not all).