> The hard part here is not finding a set of programs that always halt [...], but proving that they are correct (I'm pretty sure equivalence of primitive recurs

> The hard part here is not finding a set of programs that always halt [...], but proving that they are correct (I'm pretty sure equivalence of primitive recursive functions is undecidable). This may be true, but: If you use primitive recursive functions (instead of turing complete) because of practicality, with the same reasoning you can cap the inputs at some insanely large number. Then, these functions still "can compute anything you'd ever want to run on large inputs". In that setting, equivalence is decidable, because you can simply run both functions over the finite set of all possible inputs.