What are the practical limitations of a non-turing complete language like Coq

First, I assume you've already heard of the Church-Turing thesis, which states that anything we call “computation” is something that can be done with a Turing machine (or any of the many other equivalent models). So a Turing-complete language is one in which any computation can be expressed. Conversely, a Turing-incomplete language is one in which there is some computation that cannot be expressed.

Ok, that wasn't very informative. Let me give an example. There is one thing you cannot do in any Turing-incomplete language: you can't write a Turing machine simulator (otherwise you could encode any computation on the simulated Turing machine).

Ok, that still wasn't very informative. the real question is, what useful program cannot be written in a Turing-incomplete language? Well, nobody has come up with a definition of “useful program” that includes all the programs someone somewhere has written for a useful purpose, and that doesn't include all Turing machine computations. So designing a Turing-incomplete language in which you can write all useful programs is still a very long-term research goal.

Now there are several very different kinds of Turing-incomplete languages out there, and they differ in what they can't do. However there is a common theme. If you're designing a language, there are two major ways to ensure that the language will be Turing-complete:

• require that the language has arbitrary loops (while) and dynamic memory allocation (malloc)

• require that the language supports arbitrary recursive functions

Let's look at a few examples of non-Turing complete languages that some people might nonetheless call programming languages.

• Early versions of FORTRAN did not have dynamic memory allocation. You had to figure out in advance how much memory your computation would need and allocate that. In spite of that, FORTRAN was once the most widely used programming language.

  The obvious practical limitation is that you have to predict the memory requirements of your program before running it. That can be hard, and can be impossible if the size of the input data is not bounded in advance. At the time, the person feeding the input data was often the person who had written the program, so it wasn't such a big deal. But that's just not true for most programs written today.

• Coq is a language designed for proving theorems. Now proving theorems and running programs are very closely related, so you can write programs in Coq just like you prove a theorem. Intuitively, a proof of the theorem “A implies B” is a function that takes a proof of theorem A as an argument and returns a proof of theorem B.

  Since the goal of the system is to prove theorems, you can't let the programmer write arbitrary functions. Imagine the language allowed you to write a silly recursive function that just called itself (pick the line that uses your favorite language):

  theorem_B boom (theorem_A a) { return boom(a); }
  let rec boom (a : theorem_A) : theorem_B = boom (a)
  def boom(a): boom(a)
  (define (boom a) (boom a))
  

  You can't let the existence of such a function convince you that A implies B, or else you would be able to prove anything and not just true theorems! So Coq (and similar theorem provers) forbid arbitrary recursion. When you write a recursive function, you must prove that it always terminates, so that whenever you run it on a proof of theorem A you know that it will construct a proof of theorem B.

  The immediate practical limitation of Coq is that you cannot write arbitrary recursive functions. Since the system must be able to reject all non-terminating functions, the undecidability of the halting problem (or more generally Rice's theorem) ensures that there are terminating functions that are rejected as well. An added practical difficulty is that you have to help the system to prove that your function does terminate.

  There is a lot of ongoing research on making proof systems more programming-language-like without compromising their guarantee that if you have a function from A to B, it's as good as a mathematical proof that A implies B. Extending the system to accept more terminating functions is one of the research topics. Other extension directions include coping with such “real-world” concerns as input/output and concurrency. Another challenge is to make these systems accessible to mere mortals (or perhaps convince mere mortals that they are in fact accessible).

• Synchronous programming languages are languages designed for programming real-time systems, that is, systems where the program must respond in less than n clock cycles. They are mainly used for mission-critical systems such as vehicle controls or signaling. These languages offer strong guarantees on how long a program will take to run and how much memory it may allocate.

  Of course, the counterpart of such strong guarantees is that you can't write programs whose memory consumption and running time you're not able to predict in advance. In particular, you can't write a program whose memory consumption or running time depends on the input data.

• There are many specialized languages that don't even try to be programming languages and so can remain comfortably far from Turing completeness: regular expressions, data languages, most markup languages, ...

By the way, Douglas Hofstadter wrote several very interesting popular science books about computation, in particular Gödel, Escher, Bach: an Eternal Golden Braid. I don't recall whether he explicitly discusses limitations of Turing-incompleteness, but reading his books will definitely help you understand more technical material.