> Most languages ... do not gain any benefit from this restriction. One exception is in domains where you are proving properties or doing analysis Not even the

> Most languages ... do not gain any benefit from this restriction. One exception is in domains where you are proving properties or doing analysis Not even then. In some cases you need to forbid recursion in the proof language to make it consistent if it is based on the lambda calculus, but making the object (programming) language non-Turing complete does not make analysis/proof easier, unless you consider going from potentially infinite difficulty to unbounded difficulty "easier." The complexity of analysing a program written in a language with only if/else, no recursion, not even bounded loops, and just boolean variables and no arrays is already PSPACE-complete in the size of the program. Some people think that program analysis is hard because of the halting theorem (or its corollary, Rice's theorem), but that's just the simple story told to first-year students. A generalisation of those theorems (sometimes called "bounded halting", but it's part of one of the most theorems in computer science, the time-hierarchy theorem) says, roughly, that, in the worst case, you cannot determine in under N steps whether a program will halt (/emit some output/reach a certain state) on input X within N steps. That's the "master" theorem that determines the difficulty of program analysis/proof, and not only does it hold for some of the more powerful non-Turing complete languages, it even holds for the simplest computational models: finite state machines. To give an intuition as to why termination cannot possibly make analysing programs or proving interesting properties about them, consider that we can take any program, in any language, and mechanically translate it into such a termination language (even better: into a finite state machine!) while maintaining its behaviour for all practical intents and purposes: We add a decrementing counter, initialised to, say, 2^1000, to all loops/recursive calls, and terminate the program when it reaches zero (possibly changing types to allow that, but that is easy to do even mechanically). This program will behave just like the original at least for the duration of the universe, so we don't care about any differences that could arise later. In other words, if termination (or even "finite-statedness") alone made a difference to program analysis, we can already assume, without loss of (practical) generality, that all programs are like that already. On the other hands, many specific instances of programs in either terminating or Turing-complete languages are relatively easy to analyse.