Where it is accepted that a language has to be Turing complete to be any good, is it actually possible to have a 'useful' programming language that isn't Turing complete?
I should clarify that this is quite specifically about 'programming' languages in the traditional sense, and not markup or query languages.
Best Answer
Coq, Agda, HOL and ACL2 are very useful and extremely powerful languages, although they're not Turing-complete.
A common feature that renders them non-Turing-complete is the fact that it is always possible to prove termination. A very simple limitation is enough: recursive calls are only allowed on provably structurally smaller terms. Therefore while it is not possible to implement an interpreter for a Turing-complete language or even for the language itself many other useful things are still possible, like a certified C compiler.