> If we want to reason operationally about fac5 and fac6, as you do in your Java/asserts example

I'm not reasoning operationally. I'm reasoning denotationally, in the imperative denotation (of Hoare logic). Denotational does not equal functional.

> if we're talking about things like stack depth it's definitely operational rather than denotational, that's the point of that terminological distinction

Not true. In imperative languages, the stack is a part of the state, and the state is a part of the denotation.

> The difference is that we can also reason about them denotationally

You mean using functional denotation, or equationally. The functional denotational semantics contribute, IMO, to the least tricky parts of a program, yet come for a cost (if enforced, as in Haskell; you can have pure functions in ML and Java, too). There is nothing intrinsically superior about it. It's a denotational semantics that's convenient for specific uses, and not so convenient for others. In addition, some people are aesthetically drawn to it (I guess they like thinking of computation as functions), while others, like me, are not particularly drawn to it.

> all we'd need is to define the equivalence between readFile/writeFile and get/put.

Yes, I said that can be done with, say, a free monad, but it still cannot be done to relate fac1 to fac5, even though they are the exact same algorithm.

> I mean, IO specifically is, by design, the place we put things that we don't care to ascribe formal denotational semantics to

Well, the denotational semantics for imperative languages is very easily applied to IO, and is beautifully and elegantly done in a language like Eve.

> plenty of monads form algebras that you can compare, reduce, and put in a canonical form like any other kind of expression

Sure, except that most modern programs are interactive/concurrent/distributed, and so their trickiest bits require IO and nondeterminism in general. That's why I said that languages with a mathematical framework that elegantly handles IO and nondeterminism are better suited to modern programs.

> 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.

Ah, but other formalisms allow you to reason in a simple, elegant denotation even about things that require operational reasoning in Haskell. This is exactly why Haskell degrades to something that's little better than classical imperative languages precisely where programs get interesting and tricky. I am not comparing Haskell to itself; I'm comparing it to different, newer formalisms.

> With the functional approach you effectively just write your proof and get the algorithm for free.

1. That's not due to the functional approach. You could, in principle, generate an algorithm from any constructive proof, regardless of formalism.

2. To the best of my knowledge, no one has ever done that for anything that can be considered a real, nontrivial system. Program extraction from proofs is still very much a research topic, and very far from practical use.

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

Which is why I said if the proposition is provable. This is called "relative completeness", i.e., if a proposition is provable in some formal system X, then it is also provable in my formal system Y.

> You do have to delineate your effectful parts from your pure parts

Again, you are thinking inside one particular formalism. Effects are "impure" (i.e. break the denotation) only within the functional formalism. They are perfectly pure in TLA+ or Eve precisely because their denotation is not functional, yet simple and elegant.