A guaranteed terminating version of the language

[mk270]

Would this be in some sense trivial, or should it be more useful than that? The most interesting work I've seen in the area of "maximum expressiveness while guaranteed to terminate" is Charity, which in a nutshell adds expressiveness with a neat duality: it allows (ordinary) recursive datatypes, required to be finite, operated on by primitive recursion (paramorphism; guaranteed to terminate); and corecursive datatypes (allowed to be potentially infinite) operated on by co-recursion (apomorphism; guaranteed to be productive, i.e. "to make progress"). The key is that each type of datatype can only be operated on by its corresponding control structure.

This is sufficient to write non-primitive-recursive functions such as Ackermann's.

(Unfortunately the Wikipedia page seems to have been deleted.)