> 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).
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.