This question already has an answer here:
Non-turing complete languages can solve every practical problem that a turing-complete language can. Also, they are much more analyzable than turing complete languages. The compiler can comprehend the program as a whole, predict/compute/cache every possible computation in advance, optimize it the most mathematically possible and even prove it has done so. It is like a super fusion between static typing and lazy evaluation in roids.
Yet nobody is trying to design a non-turing complete language like COQ that is practical and usable. Why?