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