Leslie Lamport: Computer Science and State Machines (2008) [pdf] | Hacker News Reader

Leslie Lamport: Computer Science and State Machines (2008) [pdf]

research.microsoft.com

46 pointspron14 comments

A while back on here, I was arguing against common methods of programming for security-critical software in favor of high assurance methods. Those methods used mathematical specification, refinement, analysis, and so on to know everything the program could do in success or failure. The implementation was similarly provable due to how it was implemented: state machines. All high assurance that I could recall used interacting state machines (ISM's or ASM's) with modularity, abstraction, and careful interfaces. I also remember being surprised that "kragen" correctly guessed FSM's as what I was advocating.

State machines are very versatile. One can do provably safe transformations on them with suitable tools. One can derive them from functional languages where most of developing and proving work is done. I've seen several techniques of high-level synthesis for hardware that produce, split, optimize, merge, etc various FSM's to go from high-level function to logic gates. Many formal verification tools, esp easier model checkers, work well with them. All this makes them a powerful tool worth mastering and using more than we do.

So how would you rank model checking, abstract interpretation and theorem proving according to your experience in terms of practicality?

Abstract interpretation (esp Astree Analyzer) at top for ease of use in static analysis. Fire and forget mostly. Model checking next because you just learn specifications and certain ways of structuring code for easy analysis. Theorem proving last for where it's worth the specialist labor and long turnaround (eg kernels, compilers, SSL).

That's been my order for years. Empirical evidence supports it so far.

There is an absolute goldmine of stuff here:

http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

Impressive amount of information. Seems it might take a life-time just looking through it though.

It took a lifetime to produce so that would be fair. On the plus side you can do targeted dives into the stuff that you need and/or are interested in.

> For example, a BNF grammar can be described by a state machine whose states are sequences of terminals and/or non-terminals.

Eh... for BNF grammars, you'd need a stack. Or an infinite state machine.

It's true that BNF grammars can define non-regular languages, and so can't be parsed with an FSM. I wouldn't expect Leslie Lamport to have overlooked that fact, though... Skimming, I think what's being described are infinite state machines. FTA:

"For example, a BNF grammar can be described by a state machine whose states are sequences of terminals and/or non-terminals. The set of initial states contains only the sequence consisting of the single starting non-terminal. The next-state relation is defined to contain <s, t> iff s can be transformed to t by applying a production rule to expand a single non-terminal."

Isn't a stack just a "sequence of terminals and/or non-terminals"? (Or as you suggested, an infinite state machine where the states are all possible sequences of terminals and/or non-terminals.)

A pushdown automaton's stack alphabet is arbitrary (so you could make it "terminals union nonterminals" but you don't have to) and finite (so you could not make it "all sequences" without a length cap).

I suppose you could represent a PDA as an infinite state machine but the "stack" abstraction is kept around because it's clearer/easier to reason about. See, for example, the proof that CFLs are accepted by NPDAs and its correspondence with LR0 parsing.

He's not talking about finite state machines but just state machines. He even says, right at the beginning, that Turing machines are state machines.

This guy gives me Imposter Syndrome. He had a PhD from MIT at 8 years old or something and wrote the code that verifies the correctness of AWS, Turing Award. What am I doing with my life?

He's just a man, and has probably made considerable sacrifices to be at the pinnacle of CS research. Last year I saw him present a talk that was rather underwhelming (maybe I'm just dumb) - if that anecdote helps humanize him to you.

"What am I doing with my life?"

Finding a more suitable reference point, I hope. If everyone who isn't Leslie Lamport is a failure, you're not an imposter - you're playing the role of a failure like the rest of us.

Reply on news.ycombinator.com