[0] https://en.wikipedia.org/wiki/Total_functional_programming

But sometimes it is hard, and I'm afraid it's equivalent to the halting problem in general case.

Without recursion, though, finding the maximal depth of the call graph is definitely solvable, and likely not even very hard.

Side note: an interesting case is the Stable Marriage Problem. It's easy to write the O(n) algorithm and prove its bound, but it's hard to translate into a bounded recursive algorithm that does the same thing.

(At least as far as I understand -- I searched it on Stack Overflow and that's what it said, and I've tried the problem itself. A Coq fanatic insisted that "if you can prove the run time is bounded it's easy to write the bounded recursive equivalent" but somehow that never translated into an actual insight on how to do it.)

There are still cases where you can prove that a recursion is bounded (I suppose something like dependent types could help here). There are definitely cases where you can prove that a loop is bounded, because the semantics of the language requires them to: a loop with a counter (not otherwise mutated), iteration over a known finite structure, etc.

Well, both C++ and Haskell allow you to use compiler features that are undecidable in general case, but usually work well in practical cases. Also, if e.g. your recursion / loop analysis is taking too long, you can just stop the analyzer. If the code can't be reasonably proved right, it should be considered wrong (with a chance of a false negative).