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