I still don't see what you're claiming (and I certainly don't see it as involving any equivalence between recursion and the state monad). If we want to reason operationally about fac5 and fac6, as you do in your Java/asserts example (if we're talking about things like stack depth it's definitely operational rather than denotational, that's the point of that terminological distinction), it's no harder to do that in Haskell; everything you've written there would translate very directly. The difference is that we can also reason about them denotationally; all we'd need is to define the equivalence between readFile/writeFile and get/put. I mean, IO specifically is, by design, the place we put things that we don't care to ascribe formal denotational semantics to, but that's not true for monads in general; plenty of monads form algebras that you can compare, reduce, and put in a canonical form like any other kind of expression; State has canonical semantics as a function and has its equivalence defined like the equivalence of functions (which are of course not something we can compare directly for equality, but that equality is still well defined - just not always provable). For an even clearer example, Writer literally is just a pair of values, and you can compare two Writer values directly for equality like any other value.

Monads are a convenient tool for managing effects that we want to reason about operationally - they allow us to divide our program into a fragment we reason about denotationally and a fragment we reason about operationally - so you often see them used for that kind of effect, but to imagine that there's any difficulty in reasoning about them denotationally is to get it backwards.

> There is a way to relate fac5 and fac6, but that requires rewriting them and extracting some common monad (maybe the free monad?) that will give them both the same denotation.

You could write the function polymorphically (that's basically all final tagless style is). Or you could use a free monad as you suggest. Either way you can write expressions in terms of a set of effects (using coproducts in the general version of the free case) and then define the implementation of those effects later.

> For example, in TLA+ (or even in Java, as you’ll see below), you just write your algorithm and then prove whatever it is that you want,

True enough, but at the cost of doing twice as much work. With the functional approach you effectively just write your proof and get the algorithm for free.

> and if your proposition is provable, this can always be done, by some completion theorems.

Surely this can't be true in general - doesn't the halting problem make it impossible?

> However, in Lean, or let alone in Idris, you have to write your program with what you want to prove about it in mind. Oh, you also want to state a proposition about complexity? You have to rewrite the program with types that express complexity.)

True up to a point. You do have to delineate your effectful parts from your pure parts, and your pure parts are permanently pure since the pure fragment of the language has a very broad set of equivalences - as with any equivalence there's no way to make it unequivalent after you've used it in reasoning, so there's no way to recover a distinction between effects of pure code. It's the same for any kind of program analysis though - if you want to analyse the complexity of a program you can't reuse any of the analysis you did of some previous program property, you have to re-analyse every single function in terms of the new effect. So isn't it the same piece of work either way?

But yeah, introducing this very broad equivalence has its costs - but without it you're left dealing with a space of possibilities that's far too large to reason about.