It is well known that primitive recursion is not powerful enough to express all functions, Ackermann function being probably the best known example. Now, in the logic courses (that I have had look at) one always proceeded from primitive recursion to mu-recursion. In computer science terms this basicly means we are jumping from a formalism where programs are quaranteed to halt to a Turing-complete formalism where halting is a non-computable property i.e. we can't say for every program if it will eventually halt. I got curious if there is any hierarchy between primitive recursion and mu-recursion. After a while I found a programming language called Charity. In Charity (according to Wikipedia) all programs are quaranteed to stop, thus its not Turing-complete, but, on the other hand, it is expressive enough to implement Ackermann function. This suggests there is at least one level between mu-recursion and primitive recursion. My question is: does there exists any other halt-for-sure formalisms that are more expressive than primitive recursion? Or, even better, does there exist some known hierarchies between mu-recursive and primitive recursive functions? I'm curious about how "much" we can compute with a formalism that guarantees halting.