<p><pre><code>    You cannot use formal equivalence to prove 
</code></pre>
I&#x27;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.<p>So in a hard way, the complexity of <i>formal</i> reasoning about the correctness of loops and recursion must be the same.