Computation and State Machines (2008) [pdf]

Computation and State Machines (2008) [pdf](lamport.azurewebsites.net)

83 points by bechap 7 years ago | 8 comments

Is TLA+ is the culmination of Leslie Lamport's approach to describing state machines?

https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7...

pron 7 years ago | |

Well, he's worked on it for ~25 years...

bluenose69 7 years ago |

For HNers who use citation tools, a relevant RIS item for this may be as follows (sorry, had to edit to try to get it to format reasonably)

    TY  - MANSCPT
    TI  - Computation and State Machines
    AU  - Lamport, Leslie
    AB  - I have long thought that computer science is about concepts, not languages. On a visit to the University of Lugano in 2006, the question arose of what that implied about how computer science should be taught. This is a first, tentative attempt at an answer.
    DA  - 2008/04//
    PY  - 2008
    UR  - https://www.microsoft.com/en-us/research/publication/computation-state-machines/
    ER  -

Varghammer 7 years ago |

Didn't get it. State machines are the very first basics of any degree in computer science. You learn that such models are the basis for any computation. You also learn that no one uses such formalizations in practice because they are way too complex.

pron 7 years ago | |

First, I'm not sure this is the case here, but people often confuse finite state machines with state machines (which potentially have an infinite state space).

Second, the translation from a programming language to a state-machine formalization (i.e., with an initial state set and a next-state relation) is not only relatively simple, but the result is often very succinct and clear, as those who use TLA+ can testify. It is true that very few people, comparatively speaking, use mathematical formalization of any kind, but among those who do, the state-machine formalization is the most popular by a wide margin.

Jtsummers 7 years ago | |

I use state machines in my work (or did, less programming these days). They're an impressively effective formalism for modeling systems at various degrees of complexity.

What state is my radio in? When I receive this message what state does it move into? When I send this message what state does it move into? Etc.

Even if our programs aren't direct translations of this model, our specification comes out this way (or is better understood if you view it this way). All of our simulators take this model directly. Our automated testing, similarly, is done by using this state machine model of the system.

nabla9 7 years ago | |

Maybe that's the problem. They teach you the core concept, then you graduate believing that it's just a concept to know and hard to use, because you think that programming with state machines forces you to think in small state transitions and you can't abstract.

pron 7 years ago | | |

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

TY - MANSCPT TI - Computation and State Machines AU - Lamport, Leslie AB - I have long thought that computer science is about concepts, not languages. On a visit to the University of Lugano in 2006, the question arose of what that implied about how computer science should be taught. This is a first, tentative attempt at an answer. DA - 2008/04// PY - 2008 UR - https://www.microsoft.com/en-us/research/publication/computation-state-machines/ ER -