[conceit]

Wasn't me, but it's probably because iterative loops are believed to be easier to reason about. OTOH the recursive definition for the Fibonacci or factorial numbers seem easier, for one because they map to the literal explanation.

[mafribe]

    iterative loops are believed to be easier to reason about.

This cannot be the case, because you can translate loops into recursion and vice versa, so every reasoning problem that one finds with loops is also a problem in reasoning about recursion and vice versa. If you look at the Hoare-logic rules this shows up clearly. In both case you need a suitably invariant, and you need a termination argument.

[conceit]

Does the translation come for free? If not, it's probably complicated to reason about.