Between mu- and primitive recursion 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.
 A: The class PR of primitive recursive functions is the smallest class of functions containing a few simple functions (successor, zero, projection) and closed under composition and definition of functions by recursion. 
If $f:\mathbb{N}^k\to \mathbb{N}$ is any function at all, one can form the class $PR(f)$ of functions that are primitive recursive relative to $f$, simply by adding $f$ as one of the simple functions and then closing under composition and recursion. If $f$ is total, then every function in $PR(f)$ is total, and if $f$ is computable, then every function in $PR(f)$ will be computable. This amounts to using $f$ as an oracle, as mentioned by Max. There is a clear hierarchy here, because if $f\in PR(g)$, then $PR(f)\subset PR(g)$, and this hierarchy amounts to something like the hierarchy of Turing degrees, but with primitive recursion. 
More generally, for any set $F$ of functions, we may form $PR(F)$ by adding all the functions in $F$ and closing under composition and recursion, and we still have the hierarchy that if $F\subset PR(G)$, then $PR(F)\subset PR(G)$. This more general situation seems fully general, since if you have a class $F$ of functions containing all primitive recursive functions and closed under composition and recursion, then $F=PR(F)$, and so this hierarchy seems to capture all the classes that you might wish to consider.
A: I'm aware that I'm replying to a very old question and that the original poster is not even on MO any more, but for the sake of completeness, since the term did not occur in the other answers, a keyword here is "subrecursive hierarchies", and Joel Robbin's doctoral dissertation is entirely about working out the connection between classes of nested recursion, the extended Grzegorczyk hierarchy of fast-growing functions, and transfinitely adding universal functions, all being indexed by ordinal notations.
One standard class between primitive recursive and general recursive/computable is the class of functions provably total in Peano arithmetic, or $\varepsilon_0$-recursive functions.
A: Look for John Reynolds paper "Total functional programming" which is about a programming language in which only primitive recursive functions in a setting where higher-order types (like in Gödel's system T) are allowed.  Maybe that resembles Charity which Kow mentioned.   Reynolds cites a theorem (of Spector?) saying the functions his language can express are exactly the ones provably total in second-order arithmetic.  That is enormous compared with Ackermann's function but still stops short of various total functions that can be implemented on general Turing machines.
A: I think it would also be reasonable to (explicitly) mention the functions definable by primitive recursion in higher types - instead of only defining functions $\mathbb{N}\to\mathbb{N}$ by primitive recursion, we may also define families of functions (i.e. functions $\mathbb{N}\to\mathbb{N^N}$) by primitive recursion (and, of course, even more complicated things).  
As an example, let us first define an iteration function $g\colon\mathbb{N}\times\mathbb{N^N}\to\mathbb{N^N}$ by primitive recursion, by:
  \begin{array}{l}
     g(0,f) = i  \qquad\qquad\text{(the identity function)}\\\\
     g(n+1, f) = f\circ g(n, f)
  \end{array}
We can then easily define a `curried' version of the Ackermann function as a function $A\colon\mathbb{N}\to\mathbb{N^N}$, by:
\begin{array}{l}
  A(0) = S \quad\quad\text{(successor)}\\\\
  A(n+1) = g(n, A(n))
\end{array}
This is quite popular with (some groups of) computer scientists, particularly those interested in functional programming, and some form of primitive recursion in higher types is behind the strength of the language Charity you mentioned (which also allows primitive recursion over other data structures than the natural numbers).
A: Robin Chapman's answer is very apropos. Here is a theoretical answer that points out a subtlety in the question. 
First, recall that the primitive recursive functions are the smallest class of functions on $\mathbb{N}$ that:


*

*Includes the constant zero function, the successor function, and all projection functions;

*is closed under composition;

*and is closed under primitive recursion. 


Let's call this class of functions $\operatorname{PR}(\emptyset)$. For any set $A$ of number theoretic functions, we can define a more general class $\operatorname{PR}(A)$ as the smallest class of functions that satisfies the above properties and also includes every function in $A$.
If every function in $A$ is computable, then every function in $\operatorname{PR}(A)$ is computable.  Moreover, if every function in $A$ is total then every function in $\operatorname{PR}(A)$ is total. 
It would be trivial, assuming $A$ is finite (or, more generally just explicitly enumerated), to create a programming language such that every program in the language computes a function in $\operatorname{PA}(A)$ and every such function has a program in the language. The language simply has primitives for all the functions in $A$ and for the basic primitive recursive functions, along with operators for composition and primitive recursion. 
Therefore, one answer to "I'm curious about how "much" we can compute with a formalism that guarantees halting." is "For any total computable function there is such a formalism" and more generally this is true for any effective sequence of total computable functions. 
The main thing that such a system cannot have is a universal function, provided the system has some basic closure properties. 
Addendum
Since several people pointed out the same thing, I may as well add some value to the answer by including the standard proof of my remark about universal functions. A universal two-place function, for some system, is a function $g(i,k)$ such that for every one-place function $f(k)$ in the system there is some natural number $e$ with $\lambda k .f(k) = \lambda k. g(e,k)$.  Suppose that $g$ is such a function; define a function $h$ as $h(k) = g(k,k) + 1$. Then $h$ has some index $e$. Thus $g(e,e) = h(e)$ by the definition of $g$ and $e$, and $h(e) = g(e,e) + 1$ by construction of $h$. This is impossible, so any system of total functions that allows me to form the functions like  $h$ cannot have a universal function $g$. 
In particular, for any class of functions $A$ and any function $g(j,i)$ in $\operatorname{PA}(A)$, the function $h(n) = g(n,n)+1$ is in $\operatorname{PR}(A)$. So this class will not have a universal function provided that every function in $A$ is total. Of course if you let $A$ be the set of all partial computable functions then $\operatorname{PR}(A)$ is also the set of all partial computable functions and so it does contain a universal function (which is not total). 
From this point of view, the limitation is not on whether particular computable functions can be included; the limitation is on the internal structure of any particular effective class of functions. 
A: You might look up fast-growing hierarchies.
A: One can consider programming formalisms where a program is a pair (M, P), with M a Turing machine and P a proof that M halts on all inputs. Then, if the proof is correct, (M, P)(x) = M(x); if it is incorrect, (M, P)(x) = 0.
Alternatively, one can consider primitive recursion with an "oracle" function: so, for example, we can allow the Ackermann function in our recursion bounds. If we use a primitive recursive oracle, we gain no power; but as long as we use a computable function, our functions remain computable. This should give a hierarchy with respect to the oracles, but I'm not sure of the details.
A: Regarding hierarchy, it's basic result of recursion theory that every recursive function f, is expressible as:
$f(x_{0},…,x_{n}) = u(\mu y.(T(e_{f},\langle x_{0},…,x_{n}\rangle))$
where $T$, $u$ are fixed primitive recursive functions, and $e_{f}\in\mathbb{N}$ depends on $f$ (it is a code name describing how $f$ is built). (See any elementary text like Schönfield.)
Thus the hierarchy is pretty short.
