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

Fair enough, and I can see how that would allow you to defer making the choice as late as possible, in the same way as not giving a monad semantics. Still, I think the fundamental issue has to remain: if you perform an analysis that doesn't care about the state of the stack, and then want to reanalyse while considering the state of the stack, things that were equivalent in your first analysis are not equivalent in your second analysis so you can't reuse results and symmetries from the previous analysis in the new analysis. That has to be true under any formalism, any model, any what-have-you.

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

You're confusing the program with the description of the program, because of course in the lambda calculus they're one and the same. The operational semantics is the sequence of operations performed to execute the program. In the lambda calculus that happens to be the sequence of reductions, because a lambda-calculus description of a program is the program and reduction is how you execute it, but that's specific to that programming language.

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

But I thought you said I could reason about value equivalence in TLA, using your extensional equality? Certainly I want to reason that way (most of the time), because it's a lot more convenient and simpler than reasoning about sequences of operations.

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

I meant State-the-monad rather than state-the-general-concept. (Though I would say that a physical process can be a function in exactly the same sense and to exactly the same extent that it can be a computation).

> So maybe state is really and truly a function, but it's also really and truly a sequence.

Maybe it is. My point is that "The only reason monads are used in the first place is that functions cannot describe arbitrary non-sequential computation." is wrong; monads are useful for working with computations that are perfectly adequately described by functions.

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

So I think there are two different kinds of thing to talk about here: a) specific choice of formalism and model - whether that be lamba calculus, TLA or something else b) the broader notion of whether we analyse program fragments as sequences of operations on a pervasive state that changes over a pervasive time, or as expressions in a term reduction system. I'm agnostic about specific formalism, but I think being able to analyse programs as expressions where we consider expressions with the same reduction as equivalent is a vital capability that I would want any formalism I used to have. And I think there's a close-to-objective sense in which that technique/approach is valuable: the space of possibilities we have to consider when working with terms in a language can be so much smaller than the space we have to consider when working with operations on a state. (And in practice, the only form of verified formal proof of properties of program fragments that sees use in "normal" industrial code (i.e. ordinary webapps and the like, not high-assurance environments) is Haskell-like typesystems). I could believe that a different formalism could work, but I can't believe that state-based reasoning could ever displace expression-based reasoning, since (as seen in your own talk examples) even very short expressions can correspond to absolutely enormous spaces of possible states.