[skew]

Non-Turing-complete is not a bad way to go. You pretty much have to already be a researcher in dependent type systems (or maybe set theory) to invent functions that always terminate but can't be written in non-Turing-complete languages like Coq (an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of). Also, writing a program that proves some programs terminate is way easier than proving a program that correctly proves any terminating program terminates, if you are confusing the two. If it's not too common, "I didn't manage to prove this terminates" sounds like a reasonable compiler error.

[tel]

It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.

[Ono-Sendai]

Indeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..

[dllthomas]

"(an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of)"

Note, also, that there's an obvious restriction for that case to get something you can write: "evaluate for the next X steps".