6 ms·

The TLA+ Video Course by Leslie Lamport

219 points by blopeur 9y ago

ahelwer 8y ago
TLA+ is fantastic. Knowing it is like having superpowers. While others are mortally afraid of concurrency, you just spec your system & go. It also gives a huge decrease in cognitive load when you're implementing your system against a TLA+ spec. The hard stuff is already done. You can just glance at the spec to see what preconditions must be checked before an action is performed. No pausing halfway through writing a function as you suddenly think of an obscure sequence of events that breaks your code.
- polskibus 8y ago
  Are there any good tools around like c# codegen or verifiers?
  - a-saleh 8y ago
    Last time I asked aound this, the replies I got were roughly: 1. this is not the focus of TLA 2. TLA is for high-level protocol specification, there probably wont be 1 to 1 mapping to code But I know i.e. some AWS team used TLA in their project, and I would like to finde their workflow, because it is not really clear to me, how do you usually get from "This spec checks out" to "I have a working code"
    - ahelwer 8y ago
      You translate it yourself ;) you're a programmer, go program! More seriously, the main classes of bugs TLA+ defends against are logic hole bugs and concurrency bugs - spec/design bugs, the most insidious kind! That's what AWS used it for; there is no machine-enforced correspondence with the code. People get really hung up on this, but after they try to formally verify something they see the wisdom of the separation. Proving code correct is extremely time-intensive. In contrast TLA+ gives you great bang for your buck. And to repeat - translating a TLA+ spec to code is not an error-prone process and is well, well within the grasp of software engineers.
- yodsanklai 8y ago
  You make me want to give it a try. How does it compare to tools like Spin? I remember trying Spin to specify a distributed system I was working on but I didn't find it as useful as expected. If I remember well (maybe not as it was a while) the built-in concurrency model didn't really match what I was doing in my program or my programming language. It turned out my model was too far from my program to be really useful.
xuejie 8y ago
I wish Microsoft could make a new edx course in their series covering TLA+. Those lectures are gonna be more helpful with exercises one can get his/her hands dirty.
- imglorp 8y ago
  Try this https://learntla.com https://learntla.com
kornish 8y ago
Favorite comment from previous discussions: https://news.ycombinator.com/item?id=13919274 https://news.ycombinator.com/item?id=13919274 > 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. And the response: > 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. What a legend.
- baby 8y ago
  https://i.imgur.com/0gAVffm.jpg https://i.imgur.com/0gAVffm.jpg I've also noticed that sometimes the video will resize between full page and minimized, automatically when he wants you to pause the video, with relevant links below the video, what is this amazing system?
  - hood_syntax 8y ago
    I thought that resizing was really neat as well, and the videos are such a pleasure to watch. Lamport may be my favorite lecturer I never had...
mxschumacher 8y ago
this man has a wonderful sense of humor
jakeogh 8y ago
Neat. Got stuck watching Die Hard clips. Can I do all this from the CLI?
- ahelwer 8y ago
  Yes you can run the syntax & model checkers from the CLI, although then you need to manually write the model-checking settings file which I don't think the video series covers. It is covered in Lamport's Specifying Systems book, or you can take a look at the settings file generated by the GUI toolbox and adapt it to your own uses.
  - jakeogh 8y ago
    Very cool. Thank you.
baby 8y ago
https://amturing.acm.org/p558-lamport.pdf https://amturing.acm.org/p558-lamport.pdf the paper he's talking about in the first video.
CyberDildonics 8y ago
This seems to be another one of those times when everyone runs with an acronym and no one bothers to spell it out a single time. (Temporal Logic of Actions)
- monocasa 8y ago
  Three Letter Acronym

219 points by blopeur 9y ago

TLA+ is fantastic. Knowing it is like having superpowers. While others are mortally afraid of concurrency, you just spec your system & go. It also gives a huge decrease in cognitive load when you're implementing your system against a TLA+ spec. The hard stuff is already done. You can just glance at the spec to see what preconditions must be checked before an action is performed. No pausing halfway through writing a function as you suddenly think of an obscure sequence of events that breaks your code.

polskibus 8y ago
Are there any good tools around like c# codegen or verifiers?
- a-saleh 8y ago
  Last time I asked aound this, the replies I got were roughly: 1. this is not the focus of TLA 2. TLA is for high-level protocol specification, there probably wont be 1 to 1 mapping to code But I know i.e. some AWS team used TLA in their project, and I would like to finde their workflow, because it is not really clear to me, how do you usually get from "This spec checks out" to "I have a working code"
  - ahelwer 8y ago
    You translate it yourself ;) you're a programmer, go program! More seriously, the main classes of bugs TLA+ defends against are logic hole bugs and concurrency bugs - spec/design bugs, the most insidious kind! That's what AWS used it for; there is no machine-enforced correspondence with the code. People get really hung up on this, but after they try to formally verify something they see the wisdom of the separation. Proving code correct is extremely time-intensive. In contrast TLA+ gives you great bang for your buck. And to repeat - translating a TLA+ spec to code is not an error-prone process and is well, well within the grasp of software engineers.
yodsanklai 8y ago
You make me want to give it a try. How does it compare to tools like Spin? I remember trying Spin to specify a distributed system I was working on but I didn't find it as useful as expected. If I remember well (maybe not as it was a while) the built-in concurrency model didn't really match what I was doing in my program or my programming language. It turned out my model was too far from my program to be really useful.

xuejie 8y ago

I wish Microsoft could make a new edx course in their series covering TLA+. Those lectures are gonna be more helpful with exercises one can get his/her hands dirty.

imglorp 8y ago
Try this https://learntla.com https://learntla.com

kornish 8y ago

Favorite comment from previous discussions: https://news.ycombinator.com/item?id=13919274 https://news.ycombinator.com/item?id=13919274 > 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. And the response: > 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. What a legend.

baby 8y ago
https://i.imgur.com/0gAVffm.jpg https://i.imgur.com/0gAVffm.jpg I've also noticed that sometimes the video will resize between full page and minimized, automatically when he wants you to pause the video, with relevant links below the video, what is this amazing system?
- hood_syntax 8y ago
  I thought that resizing was really neat as well, and the videos are such a pleasure to watch. Lamport may be my favorite lecturer I never had...

mxschumacher 8y ago

this man has a wonderful sense of humor

jakeogh 8y ago

Neat. Got stuck watching Die Hard clips. Can I do all this from the CLI?

ahelwer 8y ago
Yes you can run the syntax & model checkers from the CLI, although then you need to manually write the model-checking settings file which I don't think the video series covers. It is covered in Lamport's Specifying Systems book, or you can take a look at the settings file generated by the GUI toolbox and adapt it to your own uses.
- jakeogh 8y ago
  Very cool. Thank you.

baby 8y ago

https://amturing.acm.org/p558-lamport.pdf https://amturing.acm.org/p558-lamport.pdf the paper he's talking about in the first video.

CyberDildonics 8y ago

This seems to be another one of those times when everyone runs with an acronym and no one bothers to spell it out a single time. (Temporal Logic of Actions)

monocasa 8y ago
Three Letter Acronym