Re:Computation and State Machines (2008) [pdf]
by pron on Tuesday September 18, 2018 @10:50AM
(#18015795)
Lamport doesn't talk about programming with state machines. He talks about coming up with a mathematical model of computation that can be both simple and with wide applicability (applies to both sequential, interactive and concurrent programs).
In such a model, state transitions can be as small or as large as you choose (e.g. sorting an array could be a single state change or multiple ones, depending on your chosen level of abstraction). Lamport's Temporal Logic of Actions (which forms the core, or at least the most interesting part of TLA+) has the very mathematical notion of abstraction as a first-class construct, i.e., A => B iff B is an abstraction of A (where => is the logical implication operator, which in TLA also means "refines" or "implements", i.e., the converse of abstraction).
In such a model, state transitions can be as small or as large as you choose (e.g. sorting an array could be a single state change or multiple ones, depending on your chosen level of abstraction). Lamport's Temporal Logic of Actions (which forms the core, or at least the most interesting part of TLA+) has the very mathematical notion of abstraction as a first-class construct, i.e., A => B iff B is an abstraction of A (where => is the logical implication operator, which in TLA also means "refines" or "implements", i.e., the converse of abstraction).