Computation and State Machines: Use math, not PLs, to think about computation [pdf] | Hacker News Reader

Computation and State Machines: Use math, not PLs, to think about computation [pdf]

research.microsoft.com

5 pointspron6 comments

My computer architecture professor had once told me, "building computers is an exercise in managing state." Over the years I've learned that this is an absolute truth. State machines are an effective abstraction in helping us reason about managing state. That said, I'm shocked at how many programmers I run into who haven't a clue about how state machines work.

If you read a bit about TLA or abstract state machines, you'll see that the premise there isn't that state machines help us reason about state, but that every computational model is an abstract state machine, from Turing machines, through process calculi, to lambda calculus (LC is a nondeterministic abstract state machine; LC + an evaluation model is a deterministic state machine). TLA unifies state machine definitions with temporal logic, in order to create a mathematical formalization of abstract state machines and their properties, and hence a mathematical formalization of computation of any kind.

In which is revealed the genesis of pron's worldview.

If by that you mean that "my" world view is based on some of the most cited publications in computer science (all by Turing Award winners), then yeah. I'm sorry to disappoint, but "my" world view is simply the mainstream world view in the software verification community, as well as in those parts of industry concerned with writing correct software (from what I can gather). I didn't realize anyone thinks there's anything particularly exceptional or controversial about it. I'm sad to say that it's nothing more than the boring mainstream view. It was Robin Milner, John Backus (also Turing award winners) and their spiritual descendants who were (and are) the daring renegades... I just find it important to mention the "classical" POV as some people -- due to whatever circumstances -- seem to believe that "mathematical" CS started with Milner (and then you start hearing strange, incorrect, stuff like "by the Curry-Howard Isomorphism, Turing completeness is isomorphic to logical inconsistency").

I really wish I could count myself a rebel and to follow Milner's vision, but, alas, in my professional life (I hope just there) I'm often a boring old fuck and a (die-hard?) pragmatist, who insists that, as cranky Dijkstra said to the visionary Backus (I'm paraphrasing), "I'll believe it when I see it". What can I say? I think Dijkstra would still be waiting. I am, however, extremely impressed with Rust :)

* https://scholar.google.co.il/scholar?cluster=243140922497407...

* https://scholar.google.co.il/scholar?cluster=110904735668495...

* https://scholar.google.co.il/scholar?cluster=135671998921191...

Oh, but things do get interesting when the relationship between languages and "concepts" (i.e. state machines) is formulated as a Galois connection (and then abstract interpretation is born). The paper that I've found most educating on the subject is this: http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4...

But yeah, I find Lamport extremely convincing (especially as his approach has been demonstrated to work well in industry and to scale to very large production systems) :)

---

P.S.

A shorter, maybe snarkier, version of this note is here: http://research.microsoft.com/en-us/um/people/lamport/pubs/d... ("Computer scientists collectively suffer from what I call the Whorfian syndrome")

Sorry if you interpreted that as some sort of criticism. That was not my intention. I'm just saying that I can now understand precisely where all your comments about state machines, proving things with simple mathematics, and disdain for languages comes from.

By the way, it also makes me cringe when I hear functional programmers talk about how useful Curry-Howard is. On the other hand I don't yet see how state machines can be more useful for my day-to-day work than PFP. I'm trying very hard though ...

> I can now understand precisely where all your comments about state machines, proving things with simple mathematics, and disdain for languages comes from.

Yep, I've been thoroughly persuaded by that work (not this particular article, which I only came across a couple of weeks ago), and am now a Lamport fanboy! I wouldn't say it's disdain for languages as much as disdain for putting languages front and center (which may -- I won't deny it -- breed a certain disdain for languages that are constantly being put front and center...).

> I don't yet see how state machines can be more useful for my day-to-day work than PFP. I'm trying very hard though ...

That may depend on what you do. You may find TLA+ or Alloy[1] extremely useful, or maybe you won't. I simply could not possibly write the complex distributed datastore I'm working on without specifying it in TLA+. Theoretically, I guess I could have used Isabelle or maybe even Coq (Vardi), but that would have taken me an order of magnitude longer to learn, and an almost unimaginable effort to actually specify (I'm unaware of such large-scale specifications in Isabelle, let alone in Coq). But my main point is this: the state machine approach isn't necessarily more useful than FP as a form of reasoning about programs (that would depend on the particular program), but it is absolutely far easier (verified by various attempts of trying to get engineers to use TLA+ vs. Coq).

I also think it is more fundamental (as FP is defined in terms of state machines, AKA a "computational process", as in http://www.paultaylor.eu/~pt/stable/prot.pdf) but not vice versa -- though it could be, with monads! -- but this is mostly a matter of taste. What I care about is ease and simplicity (which often translate to practicality).

[1]: Personally, I much prefer TLA+, if only for the elegance, minimalism and sheer power (I think it's the Lisp of mathematical specification of programs). Alloy may be better suited to some tasks, though. Learning TLA+ may make you appreciate how TLA unifies programs with properties about programs into a single concept; in a twisted way you can think of it as programming with types only.

Reply on news.ycombinator.com