Re: on termination

I don't know if this answers your question, but the class of primitive recursive programs is not the largest class of provably terminating programs there is.

For example, I can very easily produce a programming language which consists of primitive recursive programs plus these five other specific programs which I happen to know always terminate because I proved it by other means.

That's a good example. So how much can we expand this class? Is it possible to cover all recursive languages, or is there a theorem that says this is not possible?