regex - Practical non-Turing-complete languages?

Question

Nearly all programming languages used are Turing Complete, and while this affords the language to represent any computable algorithm, it also comes with its own set of problems. Seeing as all the algorithms I write are intended to halt, I would like to be able to represent them in a language that guarantees they will halt.

Regular expressions used for matching strings and finite state machines are used when lexing, but I'm wondering if there's a more general, broadly language that's not Turing complete?

edit: I should clarify, by 'general purpose' I don't necessarily want to be able to write all halting algorithms in the language (I don't think that such a language would exist) but I suspect that there are common threads in halting proofs that can be generalized to produce a language in which all algorithms are guaranteed to halt.

There's also another way to tackle this problem - eliminate the need for theoretically infinite memory. Once you limit the amount of memory the machine is allowed, the number of states the machine is in is finite and countable, and therefore you can determine if the algorithm will halt (by not allowing the machine to move into a state it's been in before).

Answer 1

Don't listen to the naysayers. There are very good reasons one might prefer a non-Turing complete language in some contexts, if you want to guarantee termination, or simplify code, for example by removing the possibility of runtime errors. Sometimes, just ignoring things may not be sufficient.

The paper Total Functional Programming argues more or less persuasively that in fact we should almost always prefer such a restricted language because the compiler's guarantees are so much stronger. Being able to prove a program halts can be significant in and of itself, but really this is the product of the much easier reasoning that the simpler languages afford. As one component in a hierarchy of languages of varying capability, the range of utility of non-universal languages is quite broad.

Another system that addresses this layering concept much more fully is Hume. The Hume Report gives a full description of the system and its five layers of progressively more complete, and progressively less safe, languages.

And finally, don't forget Charity. It's a bit abstract, but it is also a very interesting approach to a useful but not universal programming language, which is based very directly on concepts from category theory.