[Tarean]

In my head the two dimensions are tail Vs non-tail jumps, and explicit Vs implicit scope passing.

The most interesting case is implicit scope+non-tail recursion, usually this requires you to capture the variable context in mutable objects/monads/effects or similar.

This explicit capturing is neat because you still have consistent shapes for your state to define invariants over, but it's easier to decompose the logic and ignore parts of the context which are irrelevant. It lets you split problems into domain specific languages, each of which has a set of (maybe overlapping) contexts, and ideally each of which can be proven in isolation.

Also, the control flow of loops is a very restricted case of even tail jumps. Tail recursion has arbitrary jumps between basic blocks and loops are properly nested basic blocks. Even with labeled breaks, efficiently simulating arbitrary tail recursion without goto is tough. Induction proofs/data flow analysis/abstract interpretation don't care, but I'm not sure it makes proofs easier.