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.<p>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.<p>This language is a joy to use and I've found it really affects the way I think about system design.
Introduction @2:49<p>"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>..."
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.
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.
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:-)<p>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?<p>BTW, do any of my HN's fellows have a good Java state machine opens source library to recommend?
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.<p>(To understand PlusCal, you need first understand the basics of TLA+, but you don't need to understand the action system 100% in-depth.)<p>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.
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?)
> 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]<p>from wikipedia
Possibly a side question:<p>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?
the video says it's 'video#1'...
so where's the link to video#2, #3, ... ???<p>*edit: sorry I see the link after the end of video#1...