[mafribe]

    You cannot use formal equivalence to prove 

I'm afraid I have to disagree here. There is a mechanical translation from loops to recursion and back. Likewise, there is an associated mechanical translation from Hoare-triples and associated proofs for reasoning about loops to Hoare-triples and associated proofs for reasoning about recursion and back.

So in a hard way, the complexity of formal reasoning about the correctness of loops and recursion must be the same.

[AnimalMuppet]

That doesn't mean that the reasoning in a human brain is equally difficult, or equally error-prone. If nothing else, doing the transformations (and back) adds to the cognitive burden.

[mafribe]

That depends primarily on the programmer's experience, if you are used to loops but not recursion, then obviously the former is simpler than the latter, and vice versa. If you are equally familiar with both, they then thinking about it is equally difficult.