Loop invariants are a lot more intuitive if you convert your loops into while() form and then further into tail recursion - they turn into a proof by induction.

Loop invariants are a lot more intuitive if you convert your loops into while() form and then further into tail recursion - they turn into a proof by induction. For the first example, consider: go (n, i, sum): given sum = 1 + 2 + ... + i-1 returns (1 + 2 + ... + n) : per cases of (i <= n) assume (i <= n) { note: (sum = 1 + 2 + ... i-1 -> (sum + i) = 1 + 2 + ... + i) return go (n, i + 1, sum + i); } else assume (i > n) { note: thus i = n + 1 then: sum = 1 + 2 + ... + i - 1 = 1 + 2 + ... + n return sum; } sum n: returns 1 + 2 + ... + n = { note: 0 = 1 + 2 + ... + (1 - 1) // ^^^ Need to prove our precondition for go! return go (n, 1, 0); } The other examples are a bit more complex for sure, but structurally similar. It's nonetheless easy to see how even very limited changes in complexity (such as the choice of loop indexing) can create quite a few pitfalls for truly rigorous proof!