Hmm... it may be a little too late to comment on this and still be noticed, but from what I understand, not all forms of recursion are created equal, and you can do most things using total functions, that can be guaranteed to terminate. In fact, the compiler can check it automatically without any modification to your code, using a couple of known proof strategies, the simplest ones being inductive and lexicographic convergence.