Idris does that. If you add "%default total" to a file (or the equivalent compiler flag), it will make sure every function terminates unless it's annotated with "partial". In the best case, only your main function and a couple others need to be partial.