#161 overall
Specifying Systems (TLA+ video course)
Leslie Lamport
3 recommenders · 3 threads · recommended in 3 years, 2019–2022 · score 2.8
Leslie Lamport's video course introducing TLA+, a formal specification language for describing and checking the design of concurrent and distributed systems. It is distributed as a set of lecture videos alongside his TLA+ hyperbook.
Commenters call it an excellent follow-on after an introductory TLA+ course, and say it needs only basic programming background such as Python.
Algorithms & Data Structuresbeginnerfreevideo lectures#tla+#formal specification#distributed systems#concurrency#lamport
Recommendations by year
20062026
Lamport's video course is great (it's linked from the hyperbook, but just in case here's the direct link: https://lamport.azurewebsites.net/video/videos.html).
If you've used Python before that's more than enough background to get started, no other CS knowledge required.
hwayne's Learn TLA+ [0] is a very approachable introduction and survey. Lamport's TLA+ course [1] is an excellent follow on after going through Hillel's course. That link also includes the book itself.
[0] https://learntla.com/introduction/
[1] https://lamport.azurewebsites.net/tla/learning.html
Not the author, but it would take 2-3 weeks if you learn by yourself (to get real stuff done, not to be an expert), or 3 full days of hands-on training.
I would recommend Lamport's video course[1] and TLA+ hyperbook[2] (Lamport says he's stopped working on it, but it's fairly complete). Note that both Learn TLA+ and Practical TLA+ don't teach much of TLA+, but rather a language called PlusCal that compiles to TLA+. Some programmers may find it easier to start with because, unlike TLA+, PlusCal resembles a programming language (and like all programming languages, it is much more complex than TLA+, but more familiar). Hillel's book also contains some good real-life examples.
You can also find examples and various other links posted on the TLA+ subreddit[3].
[1]: http://lamport.azurewebsites.net/video/videos.html
[2]: http://lamport.azurewebsites.net/tla/hyperbook.html
[3]: https://www.reddit.com/r/tlaplus/
Wow. Did not anticipate such a long reply thread. Man it looks like I really should write up a comparison of my (amateur) experiences with TLA+ (TLC + TLAPS), Dafny, Idris, and Liquid Haskell.
Also permeakra, regardless of whether you agree with the points that pron is making here, if you ever find yourself interested in TLA+, I would highly recommend his four part TLA+ series (potentially as an intermediate step after e.g. Lamport's video course). It's absolutely fabulous.