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

No, that's just not true. If you have an order relation (a Boolean lattice, in fact), and B => C, then if A => B, then A => C. I.e., any proposition C that is true for your level-of-detail B, then it is also true for your finer level-of-detail A.

> because of course in the lambda calculus they're one and the same

This is a philosophical question, but I don't think it's accurate to say that. For one, the lambda calculus alone does not really describe a computation. Only a lambda expression combined with a state-machine -- i.e., an evaluation strategy -- defines a computation.

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

I don't know how you can say either of those things. It's true that I'm a beginner at Lean, but proving things in TLA+ is usually much easier. It's not so much a sequence vs a function, but that you naturally get this beautiful "lattice of abstraction". It allows you to prove that, say, a general description of the Quicksort, one that simply cannot be written in any programming language as it leaves unspecified how a pivot is chosen as well as other details, indeed sorts, and then you can show that a particular implementation is a refinement of that high-level description, and you automatically know it sorts correctly.

In addition, this style allows you to write your program however you like, and only then prove things about it, rather than write it with specific properties in mind (e.g., if you want to prove worst-case complexity, you must either write your program as a monad or use types that include a cost model). I've heard that some functional type theories, in particular, proof refinement logic, PRL, allows you to do the same, but it's not something that you can just do in Lean/Coq (unless you embed TLA in them).

Also, by far the most common proof technique of global program correctness (regardless of formalism) is the inductive invariant technique. Namely, say your program is P, and that your global correctness property (say, "the database is always consistent") is S, and you want to show that P => S, the inductive invariant technique finds an invariant I, such that I => S, that I is true in your initial state, and that if I is true for any state s of your program, then it is also true for any state s' reachable from s. This may not be how you prove properties of some simple functions, but it is by far the most common way to prove a global property for an entire program. Behavioral semantics makes this particularly convenient.

> monads are useful for working with computations that are perfectly adequately described by functions.

Right, but they're still part of the "functional algebra". You don't use them if your computations are represented by an entirely different algebra. They are not used in process calculi, and they are not used in TLA. They just don't serve any role whatsovever in describing computations in those mathematical theories.

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

Not exactly. A "term-reduction system", more commonly called an abstract rewriting system, is also a state machine. The difference, rather, is in denotation. Whether you're working in a system where the denotational semantics of a term is a so-called partial function, or one where the semantics of a term is different, say, a set of sequences, as in TLA.

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

You get that anyway. Even in Java. That was precisely what Christopher Strachey showed when he first introduced the term "referential transparency" to programming languages[1] -- that imperative languages are referentially transparent. In Java, if you have an expression e, you can replace any sub expression, x, with another y, that has the same denotation, without changing the denotation of e. The difference between Java, Haskell and TLA is just what that denotation is. In Haskell, it is a "partial function"; in Java it's a predicate transformer [3] (i.e., a Hoare triplet); in TLA it's a set of sequences. This choice has both aesthetic and prgamatic consequences. I completely agree that the functional denotation and the behavior denotation are both normally more convenient than a Hoare triplet.

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

This is simply not true on multiple levels. One, you always "work on terms" when working syntactically. The question is what is the semantics of the term. It is 100% false that a semantic domain of partial functions makes your state space in any way smaller than if your semantics domain is sets of behaviors. It's just not true.

> 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

This is 100% false. Haskell's type system (without clever tricks such as singleton types) is so weak that the properties it "verifies" fall far, far below what is normally regarded as "formal verification". OTOH, the most common formal verification in industry is done on hardware and realtime software systems, which normally employs model checkers, and uses temporal logic, and semantics very similar to those of TLA or Eve. Eve brings the formalism that's so far been used for formally-verified development in the safety-critical world to the mainstream. In addition, some well-known companies using formal verification, like Altran UK, use Ada SPARK, which uses Hoare logic. Haskell-style programming is just nowhere near what people call formal verification, and those who use formal verification rarely use Haskell.

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

This is just mathematically wrong, because if you think of the cardinality of functions you'd realize that it's the same as (normally bigger, actually) than that of sequences (e.g. the set of functions from the natural numbers to the natural numbers is exactly that of sequences of natural numbers). In fact, this makes it harder to create automated formal reasoning tools (model checkers and static analysis tools employing abstract interpretation) for functional languages.

You're also wrong because already that style is far more common in formal verification. You don't have to take my word for it. Here are Xavier Leroy and Simon-Peyton Jones bemoan that the state of formal methods in FP is so far behind that of even "classical" imperative programming languages [4].

[1]: https://en.wikipedia.org/wiki/Abstract_rewriting_system

[2]: https://stackoverflow.com/a/9859966/750563

[3]: https://en.wikipedia.org/wiki/Predicate_transformer_semantic...

[4]: http://homepages.inf.ed.ac.uk/stg/Milner2012/Monday_Panel-ht...