> We haven't proven that we'll never be able to create a general-purpose non-Turing-complete language.

Well, if you're referring to total languages, then they are Turing complete for all intents and purposes.

Total languages are not immune to the halting problem (or, rather, to its finite generalizations known as "bounded halting"). The classical formulation of the halting problem simply tells you that verifying a program in general is undecidable. But this is simply because a Turing machine is a finite structure that can describe an infinite one. So in some way, the halting problem is undecidable in the same way that finding the maximum or sorting an infinite list doesn't terminate. Yet once the list is finite (or the Turing machine is known to terminate), you then need to ask yourself how hard is it to find the maximum element in a finite list, how hard is it to sort it, and how hard is it to verify a program that is known to terminate? The answers to all these questions are well known, and quite different from one another. Finding the maximum takes Ω(n) (worst-case), sorting is Ω(n lg n), and verification is Ω(|S|), namely at least linear in the number of states the program takes until it terminates (this directly follows from a trivial generalization of the halting problem called "bounded halting"). So sure, total programs are known to terminate, and all we have left to do now to prove them correct is to overcome a super-exponential lower complexity bound... In practice that is just as undecidable as for programs that are not proven to terminate.

And, BTW, the lower complexity bounds for verification of finite state machines written in expressive languages is already PSPACE-complete. There cannot be a useful general programming language with verification bounds that are less than exponential (unless, that is, PSPACE=P); but that is a good thing: verification of total-functional programs is super-exponential. So my point is that even completely general verification of freakin' finite state machines is out of our reach in large-enough programs. It's doubtful you can find a useful computational model that's simpler.

Also, notice that any program could trivially be made total without changing its semantics. Give me a program you want verified, I'll add a decreasing counter starting with 10100 to all its loops/recursions, and now your program is total and you'll never know the difference. Does that make it any easier to verify?

The total-language people know this. They don't claim that this makes practical program verification any easier. In fact, the motivation for totality has nothing to do with program verification but with using C-H to prove general mathematical theorems. Non-termination, as you know, is the same as inconsistencies in those proofs (although not in proofs about programs; non-termination introduces no inconsistency to those). However, some people who are only familiar with the classical formulation of the halting theorem have concluded that totality => no halting problem => verification is possible! This is false, and was abundantly clear even in the 50s. Kurt Gödel, in a letter to von Neumann in 1956, mentions in passing this finite (and obvious) generalization of the halting theorem before raising (for the first time!) the question of P vs. NP.