> The only difference in this paper is that Lamport insists that programs should be syntactically represented as state machines

Just to make sure: He does not intend for compilable programs to be represented as TLA formulas, just as electrical circuits are not laid out with ODEs. He says that reasoning about the properties of programs should be done in a system like TLA, just as electrical circuits can be modeled as ODEs. TLA+ itself comes with a tool that lets you write specification in a syntax called PlusCal, which is similar to familiar imperative languages, and Lamport himself says that he made that language because that syntax may be more convenient for some tasks.

> while most PLT people would insist that this is too much of a restriction.

Reasoning syntactically about a program in its ready-for-construction source has several advantages, but I doubt anyone would view TLA as any sort of a restriction (quite the opposite: it allows to specify discrete dynamical systems that are not even computable). But the main difference for practitioners is this: TLA works today for a wide range of programs. The ideal of reasoning about programs in their source language with similar cost is far from realized. TLA succeeds in practice simply because it is far less ambitious.

> Typed programs enable more abstract programs and specifications, because the abstraction mechanism offered by types is in some sense dual to refinement.

I am not sure what you mean.

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

I am not sure you quite realize how state machines are used in TLA. You can use higher-order functions to your heart's content, as well as higher-order state machines. The machine's are abstract, and what constitutes a state is completely up to you. TLA+ is rich enough that you can write an entire program completely using pure functions, that executes as a single TLA step.

But reasoning with functions is a specific level of abstraction. TLA allows you to go arbitrarily higher or lower. Functions are too high an abstraction if you're interested to reason about, say, complexity, and they're too low an abstraction if you want to reason about interaction (where they can only constitute single monadic steps). They may be either too high or too low for concurrency. Of course, you can embed TLA in FP and vice versa, but TLA is "naturally" broader in scope.

> You cannot really hide internal states

Why not? That's what existential temporal quantification is for. `∃∃ x : F`, means that F performs its observable operation using some internal hidden state, x (∃∃ is usually written as bold ∃)

> In a typed programming language, quantification gives you the dual abstraction of restricting the users of your program.

I'm not sure exactly what you mean. You can achieve the same thing you can with types in an untyped TLA-based language like TLA+. For example, the typing judgment `f:A->B` is simply a conjunction with the proposition `f ∈ [A → B]` in TLA+. Remember that the environment is also part of the process (or machine).

> Crucially this invariant does not have to be a (bi)simulation

The concept of bisimulation is a rather complex one designed to explain the difference between trace inclusion and stronger forms of equivalence in algebraic models that do not model state explicitly (like CSP/CCS). In TLA, bisimulation and trace equivalence are the same, and simulation is just trace-inclusion. The famous result "the existence of refinement mapping" by Abadi and Lamport shows that this is complete, namely that any implementation relation "A implements B" can be modeled as "A refines B", which in TLA translates to the familiar implication operator `A ⇒ B`. So there is no such thing as two machines, one implementing the other, that cannot be expressed in this way.

> In this generality, this is only sound for typesafe clients

Again, in TLA, a "typesafe client" is no more than an assumption about the properties of the client "process". In TLA, a specification often takes the form `◻User ∧ ◻Program` or the equivalent `◻(User ∨ Program)`

> That's what makes it valuable.

I would say that in practice the opposite holds. TLA+ is used by "ordinary" engineers to reason about systems that are far larger and trickier (concurrent, distributed) than anything that is currently done by engineers using equational reasoning in typed PFP. This advantage may (or may not) be short-lived, but I think the combination of simplicity, ease of learning, and scalability both in size and in scope is precisely TLA's pragmatic edge.