I'm very much not at the level of accomplishing formal proofs. But isn't his challenge different than what he's trying to prove? I guess my objection is in the category of "even if formal proofs aren't easier in FP, it doesn't matter". In particular, when people talk about the advantages of FP and "correctness", they aren't literally talking about formal provability - they're more talking about a spectrum of correctness, that the purely functional approach catches moves more buggy behavior from runtime to compile-time, that the functional implementation is more correct, etc.

If you adopt the strict definition of "correct", then "more" correct makes no sense, of course.

I recently ported a fairly hairy lengthy algorithm from python to scala. From something with a ton of mutability, scope confusion, exceptions serving as GOTOs for business logic - into scala pure functions. The python was inscrutable with a team of people treating it gingerly. The scala is easily refactorable and each time we take another crack at it, it shrinks into smaller and smaller code (and not by using crazy Scala) and I suspect that much of the confusing hairy complexity will disappear. I don't really know how to quantify this, but I don't think it's captured from an exercise that compares difficulty in formally proving methods in IP and FP.

So yeah... it's an awesome exercise that showed a lot, and I really want to dig more into provers, but I just don't see that his "therefore" follows, that "it's (not) easier to reason about FP than imperative".