Lamport talk

gistfile1.txt

Who builds a house without drawing blueprints?

Leslie Lamport, Yammer, Jan 23 2013

Architects plan--programmers don't.  Maybe this is why programs crash and houses don't.

A blueprint for software is a spec.  Not a formal Coq-provable one, but real-world one.

Why don't programmers write specs?  
You can't code-gen from spec (retort--can't building-gen from blueprints)

Too many programmers consider thinking about the problem to be a waste of time.  Understanding requires careful thinking.

"Writing is natures way of letting you know how sloppy your thinking is" -- someone else

There's no One True Spec(tm).  Depends on what you're building.

Spectrum of specs: prose -> math-like prose -> formal verification.

Examples from TLATEX comments.  Sometimes, when behavior doesn't have one true answer, a spec is the best way to rationalize the decisions made. He chose math-like prose in the comments of the source.

This was six formal rules, plus commentary.  Commentary is neccessary for human understanding.

Why?

Easier to understand/debug the 6 rules than 800+ SLOC of the implementation.

Why not a formal spec?
Correctness not essential.
No good tools for that in this context

Next example: Javadoc (ish)

Comments easier to read than code, higher-level.

TLA+ (a proof verifier) spec was 575LOC (in TLA+, turtles, etc) and 1300+ comments.  

Someone else translated to java, claimed that it was quite straightforward.  First bug took 9 years to find.  The bug was caused by someone extending the code and ignoring the spec.

Is the blueprint metaphor wrong?  Maybe code isn't as rigid as a house.

Anecdote:  adding a trivial change to some program took a week, because he had to understand far too much context implicit in the code.

For java, he writes spec in javadoc before writing java.  Much more often than using formal specs.

Most people write a javadoc that just restates the code without providing context.  e.g. 

/**
  * deletes the file 
  */
public void delete()

Digging into the real java.io.File javadocs, what does "successful deletion mean", etc?  

What language to use for specs? -> MATH! (logic, minimal set theory, arithmetic, etc use common sense)

Your spec math language should be able to define custom math object, e.g. integral symbol.  

More discussion of TLA+ and how it lets you define complex things, in use at Amazon, Intel. Theorum provers useful.

Specifications "should" describe what, not how, but in practice most specs describe how, but at a very high level. 

TLA+ has a hard time describing algorithms without an execution pointer.

He made a pseudocode proof language for algorithms called PlusCal that has an execution pointer.  Maybe easier.

Write code in PlusCal, then translate to java.  He seems to be arguing that algorithm errors and coding errors are orthogonal.  Debug the algo in the best context for it (PlusCal), then translate to code in and IDE

Chord (DHT) was wrong the first time, but corrected via a model checker.

"Its a lot easier to prove something if its correct."

The more thorough method is proving with TLAPS after thinking you're pretty correct with the model checker (PlusCal?).

**Some demos**

Walking through the Atomic Bakery Algo in TLA+  Some simple live coding, breaking an algorithm, watching it fail the proof checker.

**End demos**

Specs won't solve all your problems--you can still have coding errors.

Q&A

Q: What do you think of BDD?  Is it better to have a provable model, or actually be able to run the specs in the same language as the code?
A: TDD is useful mostly because it makes you think before you implement.  Tests are "a piss-poor way of trying to specify something." (certainly hard algorithms)

Q: What about quickcheck from haskell/erlang?  What about fuzzing?
A: Randomly generated tests are ineffective when dealing with concurrency.  Anecdote about them not being comprehensive.

Don't write specs in a programming language.  Architects don't write blueprints in brick.

Q: It seems like you magically have a functional decomposition of what you want your model to look like.  How do you arrive at that?
A: Idk, something about thinking hard.  Feynmann method?

Q: Whats the difference between code and a sufficiently detailed spec?
A: What's the difference between an algo and a program?  Know it when I see it?  Write properties you want the system to have, not things you want it to do!?  Doesn't work.

Specs must be abstract machines.

Q: In your ideal world, would TLA+ be executable?
A: No.  Probably wouldn't generate efficient code over most problem domains.   It's executable now in the sense that you can run the model checker.  Model checker is really slow.

Q: Does TLA+ apply to distributed systems?
A: Yes.  A lot of whether you should model check has to do whether its efficient over your problem.

Q: How do you deal with your interface boundaries?
A: Try to write their spec for them as best as you can, then debug.

Q: Is the dichotomy between programming languages and spec languages inherent?
A: idk seems 30 years out at least.

FIN