> Then these refinements evidently can't model distinctions that are sometimes important.

I don't understand. A refinement is a description at a lower level of detail. It may be a little hard to imagine if you're not used to formalisms that allow for nondeterminism, but it works like this: the high level description, say, does not describe the precise state of the stack. In the TLA theory, this means that the state of the stack can be anything, and the formula describes an infinite set of behaviors for arbitrary states of the stack. A refinement that does describe the state of the stack would denote a subset of those behaviors.

> Again, that's operation rather than denotation. Terminology isn't that important, but why not use the standard terms?

Because that's just not true. The denotational semantics of the first-order logic statement over the natural numbers `x > 4 ∧ x < 8` is the set {5,6,7}. The operational semantics of, say `⊦ x > 2 ⇒ x > 1` in Peano arithmetic is the proof of that theorem. In lambda calculus, the denotational semantics of `λ x . x + 1` is the function `f(x) = x + 1`. Its operational semantics is the sequence of reductions. Your denotation and operation are dependent on the formalism, not on what it describes. The denotation of a TLA formula is, like all first-order logics, a set (actually, a class) of models that satisfy it, which, in the case of TLA is a set of infinite sequences with some equality relation over them. The operational semantics of TLA are more similar to that of formal logic, and are basically proofs. Operation and denotation are formalism-dependent.

> They're useful because they allow us to decompose a program into fragments that can be reasoned about separately.

... with functions! If your primitive building block isn't functions but sequences, then your compositions are different, your reasoning is different, your denotation is different, and you don't need monads.

> States really and truly are functions, Writers really and truly are plain values, there is no difficulty at all in describing those things in functional terms.

Computation is an abstraction of some physical process. I don't know what it means for a physical process to be "really and truly a function". Mathematics are a description of that process. You can describe the same process using different mathematical means. So maybe state is really and truly a function, but it's also really and truly a sequence. It then becomes an aesthetic and pragmatic question as to which you would choose.

> They are a real feature: computation genuinely conforms to the monad laws, and so results about monads will be true about computation. We don't have to make use of these facts if we don't want to, but they remain true.

See my paragraph above. These monad laws are true once you describe computation using functions and monads. I don't know what it means for them to be "really" true. It's really a philosophical question. In any event, once you describe computation as sequences rather than functions, monads are unnecessary. I guess the most accurate thing to say is that if one describes computation with functions, then the monad laws necessarily hold etc.

This, BTW, is one of the things Lamport always like pointing out when explaining what math is, and he always warns about confusing language, or a description, with reality.

The main thing I'm trying to do in this discussion is not to claim that another approach is universally "better" than FP, but just to dispel the false notion that the functional approach is the "right", "mathematical" way of describing computation. It is one mathematical approach, with its pros and cons, and there are others (classical imperative, process calculi, TLA etc.), with their respective pros and cons. None can be said to be universally better than the others. They can be more or less convenient depending on what it is that you want to do and your personal aesthetic preferences.