4 ms·

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 als

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.

nabla9 8y 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 8y 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).
pron 8y 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 8y 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 8y 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 8y 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).

pron 8y 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 8y 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.