> 2) QUESTION: Are there simple programming languages so that HALT restricted to them is decidable but not primitive recursive? I suspect one could contrive suc

> 2) QUESTION: Are there simple programming languages so that HALT restricted to them is decidable but not primitive recursive? I suspect one could contrive such a language so I ask for both natural and contrived examples. I like the lexicographic descent criterion as a not too contrived example of a class of programs larger than primitive recursion, and yet for which it's easy to prove termination (e.g., https://goto.ucsd.edu/~gridaphobe/liquid/haskell/blog/blog/2013/12/15/lexicographic-termination.lhs/ https://goto.ucsd.edu/~gridaphobe/liquid/haskell/blog/blog/2...). That's apparently equivalent to the class of multiply-recursive functions (https://dl.acm.org/doi/abs/10.5555/860256.860258 https://dl.acm.org/doi/abs/10.5555/860256.860258)