> The programming language theory community indeed tries to make mathematical reasoning explicit, but they're trying to make reasoning possible within the construction language (like the algebra of gears).

We discussed this point before, and this comment finally makes it clear to me why we never saw eye to eye.

Equational reasoning is a tool for reasoning about programs, but not the only tool. Lamport uses it too, in the form of refinement (this is exactly what is used in practice, outside of "educational" papers about functional programming). More importantly though, nobody insists that all reasoning has to be equational. The Hoare logic and its Owicki-Gries variant for concurrency are the grandfathers of modern program logics, which give you a very precise language (ordinary math + X, same as what Lamport wants) for reasoning about program correctness.

The only difference in this paper is that Lamport insists that programs should be syntactically represented as state machines, while most PLT people would insist that this is too much of a restriction. Typed programs enable more abstract programs and specifications, because the abstraction mechanism offered by types is in some sense dual to refinement. Types allow you to restrict client code in a lightweight way. Combined with higher-order functions (i.e., first class functional abstraction), this allows you to achieve more abstract specifications than what can be done with state machines.

If I have a program in TLA+, I represent it as a state machine and any specification I write down is essentially just a refinement of this state machine. You cannot really hide internal states, unless you can explicitly skip them via simulation (or at least that is my impression of TLA+, you are far more experienced here and very welcome to contradict me).

In a typed programming language, quantification gives you the dual abstraction of restricting the users of your program. Existential types allow you to pick an invariant relation between two implementations. Crucially this invariant does not have to be a (bi)simulation. If you look at this from a state machine perspective, then these can be two completely different state machines externally, but they are different in a way that clients can't exploit.

For a concrete example, in https://people.mpi-sws.org/~dreyer/papers/caresl/paper.pdf , the authors show refinement between flat combining and locking, as well as between a lockfree and a lock-based stack with iterators. In this generality, this is only sound for typesafe clients.

----

If this sounds overly negative and critical of Lamport's work, then I apologize. The main point I want to make is that we are using substantially the same tools. There is nobody in program verification who seriously insists that equational reasoning is the only tool the world needs. The point of equational reasoning was always that it is a lightweight method which is easily taught to ordinary programmers. That's what makes it valuable.

If you encounter a paper (typically by Richard Bird :) ), verifying complicated programs using only equational reasoning, then take this with a grain of salt. The interesting thing about such papers is that it's possible at all ("see how far you can push this idea!"), but I've yet to meet anyone who seriously insists that this is always the easiest proof you can come up with...