Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Leslie Lamport: Video course on TLA+

lamport.azurewebsites.net

Post reply on HN
Print view View original

11–20 of 78 posts

Re: Leslie Lamport: Video course on TLA+

#11

Post by djb_hackernews »

ahelwer wrote: post #4

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…

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their distributed systems. As someone that works on distributed systems that could use some formality I think TLA+ could help, however, I have a hard time really understanding it.

Do you know of any straight forward non-trivial examples? Something a little more complex than "hello world" and something that isn't abstract?

Re: Leslie Lamport: Video course on TLA+

#12

Post by noblethrasher »

rhizome wrote: post #6
algorithmsRcool wrote: post #3

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. ..."

Hmm, on the face of it that doesn't answer the question.

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.

Re: Leslie Lamport: Video course on TLA+

#14

Post by ahelwer »

tmccrmck wrote: post #9
ahelwer wrote: post #4

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…

Outside of distributed systems what is it used for? I've only ever heard of it's use in the formalization of distributed systems.

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.

Re: Leslie Lamport: Video course on TLA+

#15

Post by ahelwer »

djb_hackernews wrote: post #11
ahelwer wrote: post #4

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…

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their distributed systems. As someone that works on distributed systems that could use some formality I think TLA+ could help, however, I have a hard time really understanding it. Do you know of any straight forward non-trivial examples? Something a little more complex…

There's a few I can think of! First, the TLA+ GitHub repo has a bunch of examples[0]. The best one to start with is the Die Hard puzzle[1], where the heroes must obtain four gallons of water given only three and five gallon jugs. In the spec[2] we set up the system and specify all possible actions; then we model-check the system to see whether it can spit out an execution trace of actions to reach a state where we have four gallons of water in a jug.

The Wikipedia article also has some good example specs[3].

For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep.

[0] https://github.com/tlaplus/Examples/tree/master/specificatio...

[1] https://www.youtube.com/watch?v=6cAbgAaEOVE

[2] https://github.com/tlaplus/Examples/blob/master/specificatio...

[3]https://en.wikipedia.org/wiki/TLA+

Re: Leslie Lamport: Video course on TLA+

#16

Post by cerebraltangent »

ahelwer wrote: post #4

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…

Kindly add transcripts to this for the benefit of the hearing impaired people ?

Re: Leslie Lamport: Video course on TLA+

#17

Post by anateus »

ahelwer wrote: post #4

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…

Kind of an out of left field question: Lamport appears in a little square of video occasionally overlaid on the slides and sometimes full screen. As far as I can tell, he never recycles an outfit and seems to switch head gear regularly. The switch is often between segments that are quite short.

It feels almost like an intentional joke. Do you think that is the case? Or just even short segments were recorded on different days and Lamport like to wear all sorts of hats? That one where he's wearing a beanie and indoor sunglasses seems particularly intentional.

I've never met him, and the delivery of the lecture seems fairly dry and serious, so I can't tell :)

Re: Leslie Lamport: Video course on TLA+

#18

Post by ahelwer »

anateus wrote: post #17
ahelwer wrote: post #4

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…

Kind of an out of left field question: Lamport appears in a little square of video occasionally overlaid on the slides and sometimes full screen. As far as I can tell, he never recycles an outfit and seems to switch head gear regularly. The switch is often between segments that are quite short. It feels almost like an intentional joke. Do you think that is the case? Or just even short segments were recorded on differ…

Haha yep, it's intentional. He has a sense of humor like that. Famously, he first presented his paper on the Paxos algorithm dressed like Indiana Jones with the fictional backstory of the algorithm being an archeological discovery of the ancient parliamentary systems of the Greek island of Paxos.

Re: Leslie Lamport: Video course on TLA+

#20

Post by ahelwer »

cerebraltangent wrote: post #16
ahelwer wrote: post #4

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…

Kindly add transcripts to this for the benefit of the hearing impaired people ?

Excellent suggestion!
Post reply on HN