Coq, Agda, HOL and ACL2 are very useful and extremely powerful languages, although they’re not Turing-complete.

A common feature that renders them non-Turing-complete is the fact that it is always possible to prove termination. A very simple limitation is enough: recursive calls are only allowed on provably structurally smaller terms. Therefore while it is not possible to implement an interpreter for a Turing-complete language or even for the language itself many other useful things are still possible, like a certified C compiler.

I would think Yegge’s term “mini-language” refers to the fact that it is often useful to use a language for specific problems where the language doesn’t require turing-completeness to accomplish the task, and this goes to the heart of how non-turing complete languages can be useful. https://sites.google.com/site/steveyegge2/language-grubbing

Wikipedia answers this very well, right in line with what my gut said. First I was thinking pure math then I remembered regexp, and Wikipedia lists Epigram which I believe would be in the ‘pure math’ vein.

http://en.wikipedia.org/wiki/Turing_completeness#Non-Turing-complete_languages

Non-Turing-complete languages

Many computational languages exist which are not Turing complete. One
such example is the set of regular languages, most commonly regular
expressions, which are generated by finite automata. A more powerful
but still not Turing-complete extension of finite automata is the
category of pushdown automata and context-free grammars, which are
commonly used to generate parse trees in an initial stage of program
compiling. Further examples include some of the early versions of the
pixel shader languages embedded in Direct3D and OpenGL
extensions, or a series of mathematical formulae in a
spreadsheet with no cycles.[citation needed] In total functional
programming languages, all functions are total, and must terminate,
such as Charity and Epigram. Charity uses a type system and control
constructs based on category theory, whereas Epigram uses dependent
types.

Data languages

The notion of Turing-completeness does not
apply to languages such as XML, JSON, YAML and S-expressions, because
they are typically used to represent structured data, not describe
computation. These are sometimes referred to as markup languages, or
more properly as “data description languages”.

It also mentions data structure representations are not languages, but I would think XSLT should count as a representation of computation, XPath perhaps not based on what Yannis said above about SQL being a query language and not a computation language. Perhaps T-SQL or PL/SQL count as computation languages though since you can do a great deal of computations using their aggregates, where the generalized form of SQL doesn’t specify aggregates perhaps.

I understand SQL is quite popular among business types

Turing completeness is necessary for a language to be fit for use as a general purpose language. But it is not sufficient, i.e. just because it is Turing complete, it is not suited for every problem domain:

• Whitespace is proven to be Turing complete but is obviously unsuited for any problem domain outside of programmer entertainment.
• C++ templates have been proven Turing complete, still you wouldn’t actually ever write whole programs with them.

Conversely a DSL is suited for the problem domain it was designed for (assuming it was in fact decently designed), even without Turing completeness:

• HTML^* provides a concise way to describe a DOM tree. While JavaScript is Turing complete and can be used to do just the same, it is far more noisy and unclear
• XPath and other query languages, PCRE without embedded code and such are all powerful tools for the single job they were designed for

^* IIRC it was proven that HTML with CSS animations is Turing complete by using them to implement Conway’s Game of Life on an array of checkboxes. But the usefulness of HTML holds even in browsers that do not support CSS animations.

There actually do exist programming languages, where you can only write “efficient” programs. Efficient in this sense means that every program written in such a language represents a language in P. Bellantoni, Niggl and Schwichtenberg describe such a language here.

The C preprocessor is not Turing-complete (by design), yet it can still implement an interpreter for a language that is Turing complete (Order-the-language, as described in the documentation, is basically just a run-of-the-mill purely functional ML/Scheme type thing, and would be relatively unremarkable – probably quite nice to use – if it weren’t for the unusual implementation).

The trick behind it is similar to the arguments above about implementing any Turing machine in a finite physical universe: the C preprocessor can’t provide an infinite number of steps, or data cells, to the language, but it can:

1. provide an unreasonably large dynamic number (2^64 or so by default), large enough for solving most realistic problems using an exponential expansion process (mumble mumble lifetime of the universe mumble).

2. use an arbitrary static cap for the above number, i.e. while the number of steps must be some finite number, you can change what the specific cap is at “compile”-time by changing the static settings of the interpreter engine. Since there is no (theoretical) limit on the actual value of this cap, it can (theoretically) be extended to fit the space requirement for any terminating program.

Not to argue that Order is necessarily “useful” in itself, or that any CPP-implemented engine would be, but it’s an interesting proof of concept. It’s also supposedly dynamically typed, which is unusual for this area.

Yes, indeed it is possible to have a useful language that isn’t Turing complete. See here: http://tkatchev.bitbucket.org/tab/examples.html

Another example of a useful Turing incomplete language is SQL. (And yet another is spreadsheets like Gnumeric or Excel, though they aren’t really programming languages.)

As to why you would want a language that isn’t Turing complete: because that allows you to make some strong guarantees about runtime behavior.

Turing completeness, put plainly, means having a capacity for recursion. Having recursion means having potentially unbounded structures in memory. Since in the real world memory is not infinite, Turing completeness requires memory management and/or garbage collection.

Banning recursion is a great way to avoid the really, really hard problem of resource management.

Nota bene! Being Turing incomplete doesn’t necessarily imply that any program will necessarily terminate. A Turing incomplete language could allow evaluating an infinite lazy list.

One interesting “sub-Turing programming language” wasn’t mentioned until now so I’ll add it.

It’s called “Crema”. It describes itself as:

Crema is a LLVM front-end that aims to specifically execute in sub-Turing Complete space. Designed to be simple to learn, and practical for the majority of programming tasks needed, Crema can restrict the computational complexity of the program to the minimum needed to improve security.

It’s quite minimalistic and rather low level.

It should look kind of familiar to C developers.

It was initially funded by the Defense Advanced Research Projects Agency (DARPA) but looks quite unmaintained at the moment of writing. But maybe someone is interested nevertheless.