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.
Favorite comment from previous discussions: <a href="https://news.ycombinator.com/item?id=13919274" rel="nofollow">https://news.ycombinator.com/item?id=13919274</a><p>> 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.<p>> 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.<p>And the response:<p>> 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.<p>What a legend.
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.
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.<p>(Temporal Logic of Actions)
<a href="https://amturing.acm.org/p558-lamport.pdf" rel="nofollow">https://amturing.acm.org/p558-lamport.pdf</a> the paper he's talking about in the first video.