Not just self-recursion, but all recursion, including transitive mutual recursion. I think it may be possible to do this via strictly lexically-scoped symbols (so imagine C with no forward declarations). Might still be ways to sneak recursion in there though.

That's what fix point combinators are for. The Y combinator won't work in a language like C++, but the Z will work fine.

For example, here's Z in C++14, used to compute 5 factorial: https://godbolt.org/g/se5B8u

Yeah, I specifically had combinators in mind when considering ways to sneak recursion in. :P And it occurs to me you'd have to forbid function pointers too.

Yup, and you would probably not be able to do Object Oriented Programming either (or have to limit it horrendously), cause an object is similar to a closure, and you therefore can use it for unbounded recursion.

Yes, I meant any recursive calls via a chain of calls to other functions.

I think proving that no recursion exists should be relatively simple, just keep following the call graph and keep a set of the nodes (functions) called; you either reach the terminal node(s), or reach an already-visited node again, which means a recursion exists.

What if functions are first class? Then imagine a function gets passed in as an argument and called. You won't know what function you're calling until runtime.

I thought that self recursion was fine so long as the calls were provably "smaller problems" than the function calling them, something like "bounded recursion".

You might be thinking of Total Functional Programming [0] "a programming paradigm that restricts the range of programs to those that are provably terminating."

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

If you can prove that the recursion is bounded, great!

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.

Really? I thought the problems were equivalent, of proving that e.g. a loop vs its recursive equivalent were bounded.

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.)

In general case, yes, of course.

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).

Proving that a loop is bounded is also undecidable.

Only in the general case. In many/most loops that humans would find useful in practice you can prove termination.