14 ms·

Leslie Lamport: Video course on TLA+

328 points by kelvich 10y ago

algorithmsRcool 10y ago
Introduction @2:49 "What kind of clown am I claiming that I know what can make you think better? ... This is not the time to be modest. I have done seminal research in the theory of distributed and concurrent systems for which i won the turning award. You can stop the video now and look me up on the web. <long pause>..."
- rhizome 10y ago
  Hmm, on the face of it that doesn't answer the question.
  - noblethrasher 10y ago
    The claim is that what he is about to say is worth your attention. Achievement of the highest professional accolade for the very stuff that he plans to discuss is literally prima facie evidence in support of that claim.
    - macintux 10y ago
      The transcription ("turning award" instead of "Turing award") makes it easier to miss the key point.
setheron 10y ago
I viewed this original when he posted them on the newsgroup. I thought they were very well done, funny and enjoyable. I still haven't applied TLA+ into something at work however I enjoyed learning it nevertheless.
ahelwer 10y ago
Great to see this here! I act as a TA for Dr. Lamport's TLA+ courses at Microsoft, and can answer any questions y'all have. TLA+ in one sentence: it is a language used to write specifications, same as you might write a spec in English/your chosen informal language, except here you write your spec in basic mathematics; benefits of a formal specification language include freedom from ambiguity, model-checking, and even machine-checked proofs of correctness. This language is a joy to use and I've found it really affects the way I think about system design.
- tmccrmck 10y ago
  Outside of distributed systems what is it used for? I've only ever heard of it's use in the formalization of distributed systems.
  - ahelwer 10y ago
    You are correct the language really shines when there is concurrency (not necessarily just distributed systems), because validating system invariants with the model-checker is just magical. I've also found the language to hold great value for specifications as such; Dr. Lamport seems to believe that most technical problems just disappear when you precisely identify what it is you want to do, and writing a TLA+ spec is an efficient way of accomplishing that. So, I've found it useful to write specs for solutions to very technical problems simply to clarify my thinking and root out areas of sloppiness.
    - ausimian 10y ago
      I concur with both these statements, but would widen the former slightly to say that it helps you think (and then validate your thinking) about any non-trivial state-machine - it doesn't have to be concurrent or distributed. [Used to work at Microsoft, used TLA+ successfully during product development]
  - hwayne 10y ago
    I've personally found it absolutely fantastic for modeling business logic. It's also really good for any kind of concurrent system, which covers pretty much every webtech startup.
  - pron 10y ago
    Indeed, TLA+ is mostly known for formalizing and verifying distributed systems and concurrent algorithms. This has a few reasons: 1. Lamport's algorithmic work is in concurrent and distributed algorithms, and as he uses TLA for his own algorithms -- and he's TLA+'s first user -- that's how it's known. 2. Few other general software verification formalisms are able to handle concurrency as easily as TLA, so that is where it shines in comparison. Of course, this is intentional because Lamport designed TLA+ to work well for the kinds of algorithms he's interested in. 3. When engineers write software systems that are too complex or subtle to be obviously correct, and could therefore benefit from formal verification, it is usually the case that a concurrent or distributed algorithm is involved. Having said that, there is nothing specific about TLA+ that makes it any less suitable for sequential algorithms. If you write one that you think is complicated or subtle enough to require help in reasoning, you could certainly benefit from TLA+. But if you're interested just in sequential algorithms, you do have more options, like Why3/WhyML, which I think is very nice (although I prefer TLA+). Whether WhyML or TLA+ would be better suited to verify your sequential algorithm depends largely on personal aesthetic preferences, as well as some details of requirements. For example, WhyML can generate OCaml code, while TLA+ can't. On the other hand, TLA+ has both SMT solvers and a model checker, which makes it more likely that you can verify the entire algorithm automatically, while WhyML requires manual proof in Isabelle or Coq for properties the automatic solvers can't verify (I hear they're working on a proof language directly in Why; I hope it's as nice as TLA+'s proof language). Also, TLA+ lets you describe your algorithm at various levels of abstraction, and show that the more detailed ones implement the more abstract ones. WhyML is more focused on the abstraction level of actual program code.
Ambrosia 10y ago
Relevant: http://sam.js.org http://sam.js.org
shaunxcode 10y ago
These are great so far! I wish you had posted about it once they were all available though as I was fully prepared to binge watch.
neves 10y ago
I'm about to start a new system that will have a state machine. The videos are really good to help to think about the problem. This guy didn't get a Turing Prize for nothing:-) I won't even try to use TLA+ in my business context. Just will search for a good java library. Maybe these videos will help me to recognize a good one? BTW, do any of my HN's fellows have a good Java state machine opens source library to recommend?
- whitenoice 10y ago
  You could use akka[1] library to build a state machine, actor model is great for building state machines [2]. I have built one in the past using akka. Library is pretty robust and well maintained. [1] http://akka.io http://akka.io [2] http://erlang.org/documentation/doc/4.8.2/doc/design_principles/fsm.html http://erlang.org/documentation/doc/4.8.2/doc/design_princip... [3] http://doc.akka.io/docs/akka/current/java/fsm.html http://doc.akka.io/docs/akka/current/java/fsm.html
  - neves 10y ago
    It looks nice, but overkill for my application. For now I have no need for distributed systems, probably some concurrency in the near future.
Avshalom 10y ago
So how amenable is tla+ to automatic translation to an existing programming language?
- ahelwer 10y ago
  Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.
  - pron 10y ago
    Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter). C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1... Java: http://ieeexplore.ieee.org/document/6042069 http://ieeexplore.ieee.org/document/6042069 The C work seems more thorough.
    - ahelwer 10y ago
      Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.
- hwayne 10y ago
  IMO not very. It's easy in TLA+ to write things like "randomly select some bijective function from the power set of N to [0, 1]", which can be really handy for speccing but isn't exactly programming-friendly. I personally think of this as a good thing, actually. TLA+ can be simpler and more expressive than it would be if it had to also be translatable. So you can't guarantee your implementation matches your spec. All the more reason to write unit tests!
  - pron 10y ago
    That is not such a big problem. Many operators in TLA+ -- like division -- are defined in terms of CHOOSE, but that doesn't stop TLC from implementing them efficiently. It's very easy to supply efficient implementations for various built in constructs, and tell you that you shouldn't use CHOOSE in your own definitions that you want to be automatically translated. So the data and data operations aren't the big problem; the control state is a bigger problem: It is hard to translate TLA+ constructs to programming language idioms like subroutines, loops and threads.
rebootthesystem 10y ago
In many ways this is what APL was originally about. Ken Iverson used it to describe the operation of early IBM computers while at IBM.
- qznc 10y ago
  "A Formal Description of System/360" Readable (kind of) here: https://www.yumpu.com/en/document/view/40763566/a-formal-description-of-system-360 https://www.yumpu.com/en/document/view/40763566/a-formal-des...
  - rebootthesystem 10y ago
    Nice find!
deleted 10y ago
[deleted]
gizmodo59 10y ago
Just finished the first video. Very nicely done. The website is nicely done too, not obtrusive and makes the learner to focus on the video. +1
mooneater 10y ago
Ok I would love to know more about how the RTOS code was shrunk by 10x using TLA+ (at 8:28)
- pron 10y ago
  Well, that book costs $99: http://www.springer.com/us/book/9781441997357 http://www.springer.com/us/book/9781441997357 But there's been more recent work done in TLA+ on another realtime OS, where the mechanical proof system, TLAPS, was used to prove some aspects of the kernel correct, and you can read about it for free here: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html
devdoomari 10y ago
the video says it's 'video#1'... so where's the link to video#2, #3, ... ??? *edit: sorry I see the link after the end of video#1...
baby 10y ago
> TLA+ (pronounced as tee ell a plus, /ˈtiː ɛl eɪ plʌs/) is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode[4] and blueprints for software systems.[5] from wikipedia
colanderman 10y ago
While TLA+ itself is great, I suspect for many here that PlusCal (a "veneer" on top of TLA+) is more immediately useful. I didn't fully grasp either language until I understood PlusCal for what it is: a simple procedural language with two nondeterministic constructs, which can be used for describing concurrent state machines. Nothing more, nothing less. (To understand PlusCal, you need first understand the basics of TLA+, but you don't need to understand the action system 100% in-depth.) The idea behind PlusCal is to write your algorithm in it, leaving out the "unimportant" bits, and using the nondeterministic operators in place of any value that is not in your algorithm's control. The model checker, TLC, can then run all possible traces of your algorithm to search for conditions under which it may deadlock or violate some assertion you have made.
nchuhoai 10y ago
Possibly a side question: What do people think of the format? I have off and on been thinking about a format where the video is the main highlight, but is supported, like this one, with links and other media to make it a more engaging experience. Are there other use cases that you think this would be conducive for?
sdbbp 10y ago
In my experience, writing a formal specification _once_ in TLA+ has shaped my mindset around architecture, implementation, and verification of distributed systems for the last 19 years. It's easier to provide feedback on most informal architecture specifications. It is easier to implement to a specification so as to have a higher confidence of compliance. It is easier to consider the state space of an architecture (distributed system) when in a testing/verification role.
Aclassifier 10y ago
I watched this very interesting and amusing series of videos and learned a lot from them. I was shown practical in-use and the motivation for mathematical syntax. I know Promela and CSPm some so I was curious to see more than a trivial example of some C lines becoming a TLA+ spec. I missed real-life examples of down-to-earth usage. The "Formal Development of a Network-Centric RTOS" book shows not only TLA+ but also why in their situation TLA+ was more suitable then other methodologies. Still, on TLA+ I miss the forest for the trees. I probably need more time with Lamport. I hope he's able to do a follow-up. (Or am I unfair here?)

328 points by kelvich 10y ago

Introduction @2:49 "What kind of clown am I claiming that I know what can make you think better? ... This is not the time to be modest. I have done seminal research in the theory of distributed and concurrent systems for which i won the turning award. You can stop the video now and look me up on the web. <long pause>..."

rhizome 10y ago
Hmm, on the face of it that doesn't answer the question.
- noblethrasher 10y ago
  The claim is that what he is about to say is worth your attention. Achievement of the highest professional accolade for the very stuff that he plans to discuss is literally prima facie evidence in support of that claim.
  - macintux 10y ago
    The transcription ("turning award" instead of "Turing award") makes it easier to miss the key point.

setheron 10y ago

I viewed this original when he posted them on the newsgroup. I thought they were very well done, funny and enjoyable. I still haven't applied TLA+ into something at work however I enjoyed learning it nevertheless.

ahelwer 10y ago

Great to see this here! I act as a TA for Dr. Lamport's TLA+ courses at Microsoft, and can answer any questions y'all have. TLA+ in one sentence: it is a language used to write specifications, same as you might write a spec in English/your chosen informal language, except here you write your spec in basic mathematics; benefits of a formal specification language include freedom from ambiguity, model-checking, and even machine-checked proofs of correctness. This language is a joy to use and I've found it really affects the way I think about system design.

tmccrmck 10y ago
Outside of distributed systems what is it used for? I've only ever heard of it's use in the formalization of distributed systems.
- ahelwer 10y ago
  You are correct the language really shines when there is concurrency (not necessarily just distributed systems), because validating system invariants with the model-checker is just magical. I've also found the language to hold great value for specifications as such; Dr. Lamport seems to believe that most technical problems just disappear when you precisely identify what it is you want to do, and writing a TLA+ spec is an efficient way of accomplishing that. So, I've found it useful to write specs for solutions to very technical problems simply to clarify my thinking and root out areas of sloppiness.
  - ausimian 10y ago
    I concur with both these statements, but would widen the former slightly to say that it helps you think (and then validate your thinking) about any non-trivial state-machine - it doesn't have to be concurrent or distributed. [Used to work at Microsoft, used TLA+ successfully during product development]
- hwayne 10y ago
  I've personally found it absolutely fantastic for modeling business logic. It's also really good for any kind of concurrent system, which covers pretty much every webtech startup.
- pron 10y ago
  Indeed, TLA+ is mostly known for formalizing and verifying distributed systems and concurrent algorithms. This has a few reasons: 1. Lamport's algorithmic work is in concurrent and distributed algorithms, and as he uses TLA for his own algorithms -- and he's TLA+'s first user -- that's how it's known. 2. Few other general software verification formalisms are able to handle concurrency as easily as TLA, so that is where it shines in comparison. Of course, this is intentional because Lamport designed TLA+ to work well for the kinds of algorithms he's interested in. 3. When engineers write software systems that are too complex or subtle to be obviously correct, and could therefore benefit from formal verification, it is usually the case that a concurrent or distributed algorithm is involved. Having said that, there is nothing specific about TLA+ that makes it any less suitable for sequential algorithms. If you write one that you think is complicated or subtle enough to require help in reasoning, you could certainly benefit from TLA+. But if you're interested just in sequential algorithms, you do have more options, like Why3/WhyML, which I think is very nice (although I prefer TLA+). Whether WhyML or TLA+ would be better suited to verify your sequential algorithm depends largely on personal aesthetic preferences, as well as some details of requirements. For example, WhyML can generate OCaml code, while TLA+ can't. On the other hand, TLA+ has both SMT solvers and a model checker, which makes it more likely that you can verify the entire algorithm automatically, while WhyML requires manual proof in Isabelle or Coq for properties the automatic solvers can't verify (I hear they're working on a proof language directly in Why; I hope it's as nice as TLA+'s proof language). Also, TLA+ lets you describe your algorithm at various levels of abstraction, and show that the more detailed ones implement the more abstract ones. WhyML is more focused on the abstraction level of actual program code.

Ambrosia 10y ago

Relevant: http://sam.js.org http://sam.js.org

shaunxcode 10y ago

These are great so far! I wish you had posted about it once they were all available though as I was fully prepared to binge watch.

neves 10y ago

I'm about to start a new system that will have a state machine. The videos are really good to help to think about the problem. This guy didn't get a Turing Prize for nothing:-) I won't even try to use TLA+ in my business context. Just will search for a good java library. Maybe these videos will help me to recognize a good one? BTW, do any of my HN's fellows have a good Java state machine opens source library to recommend?

whitenoice 10y ago
You could use akka[1] library to build a state machine, actor model is great for building state machines [2]. I have built one in the past using akka. Library is pretty robust and well maintained. [1] http://akka.io http://akka.io [2] http://erlang.org/documentation/doc/4.8.2/doc/design_principles/fsm.html http://erlang.org/documentation/doc/4.8.2/doc/design_princip... [3] http://doc.akka.io/docs/akka/current/java/fsm.html http://doc.akka.io/docs/akka/current/java/fsm.html
- neves 10y ago
  It looks nice, but overkill for my application. For now I have no need for distributed systems, probably some concurrency in the near future.

Avshalom 10y ago

So how amenable is tla+ to automatic translation to an existing programming language?

ahelwer 10y ago
Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.
- pron 10y ago
  Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter). C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1... Java: http://ieeexplore.ieee.org/document/6042069 http://ieeexplore.ieee.org/document/6042069 The C work seems more thorough.
  - ahelwer 10y ago
    Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.
hwayne 10y ago
IMO not very. It's easy in TLA+ to write things like "randomly select some bijective function from the power set of N to [0, 1]", which can be really handy for speccing but isn't exactly programming-friendly. I personally think of this as a good thing, actually. TLA+ can be simpler and more expressive than it would be if it had to also be translatable. So you can't guarantee your implementation matches your spec. All the more reason to write unit tests!
- pron 10y ago
  That is not such a big problem. Many operators in TLA+ -- like division -- are defined in terms of CHOOSE, but that doesn't stop TLC from implementing them efficiently. It's very easy to supply efficient implementations for various built in constructs, and tell you that you shouldn't use CHOOSE in your own definitions that you want to be automatically translated. So the data and data operations aren't the big problem; the control state is a bigger problem: It is hard to translate TLA+ constructs to programming language idioms like subroutines, loops and threads.

rebootthesystem 10y ago

In many ways this is what APL was originally about. Ken Iverson used it to describe the operation of early IBM computers while at IBM.

qznc 10y ago
"A Formal Description of System/360" Readable (kind of) here: https://www.yumpu.com/en/document/view/40763566/a-formal-description-of-system-360 https://www.yumpu.com/en/document/view/40763566/a-formal-des...
- rebootthesystem 10y ago
  Nice find!

deleted 10y ago

[deleted]

gizmodo59 10y ago

Just finished the first video. Very nicely done. The website is nicely done too, not obtrusive and makes the learner to focus on the video. +1

mooneater 10y ago

Ok I would love to know more about how the RTOS code was shrunk by 10x using TLA+ (at 8:28)

pron 10y ago
Well, that book costs $99: http://www.springer.com/us/book/9781441997357 http://www.springer.com/us/book/9781441997357 But there's been more recent work done in TLA+ on another realtime OS, where the mechanical proof system, TLAPS, was used to prove some aspects of the kernel correct, and you can read about it for free here: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html

devdoomari 10y ago

the video says it's 'video#1'... so where's the link to video#2, #3, ... ??? *edit: sorry I see the link after the end of video#1...

baby 10y ago

> TLA+ (pronounced as tee ell a plus, /ˈtiː ɛl eɪ plʌs/) is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode[4] and blueprints for software systems.[5] from wikipedia

colanderman 10y ago

While TLA+ itself is great, I suspect for many here that PlusCal (a "veneer" on top of TLA+) is more immediately useful. I didn't fully grasp either language until I understood PlusCal for what it is: a simple procedural language with two nondeterministic constructs, which can be used for describing concurrent state machines. Nothing more, nothing less. (To understand PlusCal, you need first understand the basics of TLA+, but you don't need to understand the action system 100% in-depth.) The idea behind PlusCal is to write your algorithm in it, leaving out the "unimportant" bits, and using the nondeterministic operators in place of any value that is not in your algorithm's control. The model checker, TLC, can then run all possible traces of your algorithm to search for conditions under which it may deadlock or violate some assertion you have made.

nchuhoai 10y ago

Possibly a side question: What do people think of the format? I have off and on been thinking about a format where the video is the main highlight, but is supported, like this one, with links and other media to make it a more engaging experience. Are there other use cases that you think this would be conducive for?

sdbbp 10y ago

In my experience, writing a formal specification _once_ in TLA+ has shaped my mindset around architecture, implementation, and verification of distributed systems for the last 19 years. It's easier to provide feedback on most informal architecture specifications. It is easier to implement to a specification so as to have a higher confidence of compliance. It is easier to consider the state space of an architecture (distributed system) when in a testing/verification role.

Aclassifier 10y ago

I watched this very interesting and amusing series of videos and learned a lot from them. I was shown practical in-use and the motivation for mathematical syntax. I know Promela and CSPm some so I was curious to see more than a trivial example of some C lines becoming a TLA+ spec. I missed real-life examples of down-to-earth usage. The "Formal Development of a Network-Centric RTOS" book shows not only TLA+ but also why in their situation TLA+ was more suitable then other methodologies. Still, on TLA+ I miss the forest for the trees. I probably need more time with Lamport. I hope he's able to do a follow-up. (Or am I unfair here?)