What are the most expressive, terminating languages?

I'm less interested in languages where you can write almost anything, but then are required to write an accompanying proof that what you wrote terminates.

I'm more interested in the design space of languages inherently confined to certain complexity classes by construction.

Is there any sort of theory hierarchy for sub-turing-complete languages?

There are plenty of classes of programming languages where all programs terminate. The most common form of enforcing termination is by way of types. The most well-developed theory of typing systems for terminating computation might be that of Barendregt's Lambda cube, which decomposes typing into three orthogonal axes:

• Parametric polymorphism

• Higher kinds

• Value-dependency of types

Starting from a terminating languages such as the simply typed $\lambda$-calculus, one can add any combination of those three axes and retain termination.

This has close connections with logic, via the Curry-Howard correspondence.

There are many extensions and refinements, including types that capture complexity classes.

StackExchange Computer Science Q#57015, answer score: 7