I guess that I am claiming that using Coq, Idris, Agda, etc, (in a setting where we are actually using them to prove correctness properties that are halting equ

I guess that I am claiming that using Coq, Idris, Agda, etc, (in a setting where we are actually using them to prove correctness properties that are halting equivalent), is itself a particular way of working in a language that is not Turing Complete. As an aside, "Turing complete programs" seems like a category error?