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?

marked as duplicate by m3th0dman, user40980, gnat, GlenH7, Dan Pichelman Sep 8 '13 at 17:40

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

  • 3
    I don't see how your first sentence is true. How, for instance, would you write a spell checker in a non-Turing complete language? – Steven Burnap Aug 10 '13 at 0:05
  • 4
    @StevenBurnap: realistically tho, you can have a "non-turing-complete" language by taking, say, Python, and halting the program after 10^100 instructions if it hasn't halted already: the phrase "turing complete" doesn't actually mean much for edge cases like coq – amara Aug 10 '13 at 1:31
  • 1
    @sparkleshy By that token, though, nothing's truly Turing Complete because no hardware lasts forever (not to mention that no hardware has infinite memory.) – Steven Burnap Aug 10 '13 at 1:43
  • 1
    @JosephQuinsey But can SQL solve "every practical problem"? – Steven Burnap Aug 10 '13 at 1:44
  • 1
    Well I write compilers in Coq for research purposes which is a practical useful problem, it's do-able. But the amount of pain that you have to go through with languages like coq (dependently typed) will forever bar it from general acceptance IMHO – jozefg Aug 10 '13 at 3:37

Non-turing complete languages can solve every practical problem that a turing-complete language can.

Wrong. You cannot, for example, even do something as simple as implement the game of Life in a non-Turing complete language. Why? Because the game of Life is Turing complete.

Once that hypothesis is seen to be false, the answer to the question is obvious.

  • 5
    but just like how computers actually have finite memory you should be able to implement game of life up to some limit – jk. Aug 10 '13 at 6:26
  • 4
    and its not clear that game of life is a practical problem at all. I can't think of any problem for which the game of life is a solution – jk. Aug 10 '13 at 6:27
  • 5
    @jk. The point is that if even something as simple as the game of life can't be done, what kind of useful programming abstractions would you have at your disposal? Easy things should be easy, not hard. – btilly Aug 11 '13 at 18:08
  • 1
    @btilly - Why is not possible to provide an arbitrary limit on the number of iterations? That would allow a proof termination and allow the game of life for an arbitrary number of iterations at least. – Davorak Sep 10 '13 at 18:58
  • 1
    Just because GameOfLife as a whole couldn't be implemented doesn't stop very large parts of it to be implementable in a non-Turing complete language. So maybe a language that forces non-Turing completeness wouldn't be very useful, but being able to restrict a function/procedure to be non-Turing complete could still be extremely useful (i.e. analog to how const in C++ which forbids certain operations or how unsafe in C# allows some unsafe operations). – Grumbel Oct 28 '13 at 9:29

One effort in this direction is the Hume family of languages, the last of which is Turing complete,

HW-Hume: a hardware description language — capable of describing both synchronous and asynchronous hardware circuits, with pattern matching on tuples of bits, but with no other data types or operations [27];

FSM-Hume: a hardware/software language — HW-Hume plus first-order functions, conditionals expressions and local definitions [26];

Template-Hume: a language for template-based programmimng — FSM-Hume plus predefined higher-order functions, polymorphism and inductive data structures, but no user-defined higher-order functions or recursive function definitions;

PR-Hume: a language with decidable termination — Template-Hume plus user-defined primitive recursive and higher-order functions, and inductive data structure definitions;

Full-Hume: a Turing-complete language — PR-Hume plus unrestricted recursion in both functions and data structures.


Not the answer you're looking for? Browse other questions tagged or ask your own question.