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

You can't write a function that simulates a Turing machine. You can write a function that simulates a Turing machine for 2^128 (or 2^2^2^2^128 steps) and reports whether the Turing machine accepted, rejected, or ran for longer than the allowed number of steps.

Since "in practice" you will be long gone before your computer can simulate a Turing machine for 2^128 steps, it's fair to say that Turing incompleteness does not make much of a difference "in practice".

An important class of problems that are a bad fit for languages such as Coq is those whose termination is conjectured or hard to prove. You can find plenty of examples in number theory, maybe the most famous is the Collatz conjecture

function collatz(n)
  while n > 1
    if n is odd then
      set n = 3n + 1
    else
      set n = n / 2
    endif
 endwhile

This limitation leads to have to express such problems in a less natural way in 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.

The most direct answer is: a machine/language that is not Turing complete cannot be used to implement/simulate Turing machines. This comes from the basic definition of Turing completeness: a machine/language is turing complete if it can implement/simulate Turing machines.

So, what are the practical implications? Well, there is a proof that anything that can be shown to be turing complete can solve all computable problems. Which by definition means that anything that is not turing complete has the handicap that there are some computable problems that it can't solve. What those problems are depends on what features are missing that makes the system non-Turing complete.

For example if a language doesn't support looping or recursion or implicitly loops cannot be Turing complete because Turing machines can be programmed to run forever. Consequently that language cannot solve problems requiring loops.

Another example is if a language doesn't support lists or arrays (or allow you to emulate them for example using the filesystem) then it cannot implement a Turing machine because Turing machines require arbitrary random access to memory. Consequently that language cannot solve problems requiring arbitrary random access to memory.

So, the feature that is missing that classifies a language to be non-Turing complete is the very thing that practically limits the usefulness of the language. So the answer is, it depends: what makes the language non-Turing complete?