3 ms·

Since the author hangs out here on HN, I'd like to ask: how long does it take to develop a working proficiency to model standard distributed systems (ex: a soup

Since the author hangs out here on HN, I'd like to ask: how long does it take to develop a working proficiency to model standard distributed systems (ex: a souped up key/value store)? It seems like he's written 2 books: Learn TLA+ Practical TLA+ Would there be any other resources that you'd recommend to supplement after those 2 books?

pron 8y ago
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 http://lamport.azurewebsites.net/video/videos.html [2]: http://lamport.azurewebsites.net/tla/hyperbook.html http://lamport.azurewebsites.net/tla/hyperbook.html [3]: https://www.reddit.com/r/tlaplus/ https://www.reddit.com/r/tlaplus/
- nickpsecurity 8y ago
  "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" Most evidence indicates using familiar concepts aids learning. That makes me hypothesize the best recommendation is the more mathematical ones for folks strong in math and the programmer-centric ones for those strong in that. That also implies that, for each of these formal topics, we need one version for each audience to draw more people in.
  - fizwhiz 8y ago
    Seem's like hillel's material is more approachable for people with a programming background, and pron's recommended material better for people who are more math-y. I'm likely going to start with Hillel's books to develop a working understanding and then move onto Lamport's stuff once i'm ready for a rigorous deep dive.
- fizwhiz 8y ago
  This a great wealth of resources, thank you! Off-topic: from your linked videos, this video at the 2min 49s mark had me absolutely creased lmao http://video.ch9.ms/ch9/bab3/13798ec2-8479-4062-8aaf-94215670bab3/init2.mp4 http://video.ch9.ms/ch9/bab3/13798ec2-8479-4062-8aaf-9421567...
hwayne 8y ago
In my workshops people usually start being able to apply it to their business problems by about day 3. It's actually pretty simple once you get the hang of it! After those two, I'd probably recommend the original _Specifying Systems_. It can be a tough read, but it's a comprehensive dive into how TLA+ works mathematically and everything that you can do with it. You can get it for free here: https://lamport.azurewebsites.net/tla/book.html https://lamport.azurewebsites.net/tla/book.html I'd also recommend practicing by applying it to problems you've already solved in your place of work. That way you can compare it against a real system you know inside and out. I talk more about that here: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/ Does that answer your question?
- fizwhiz 8y ago
  Sure does, thank you!

pron 8y ago

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 http://lamport.azurewebsites.net/video/videos.html [2]: http://lamport.azurewebsites.net/tla/hyperbook.html http://lamport.azurewebsites.net/tla/hyperbook.html [3]: https://www.reddit.com/r/tlaplus/ https://www.reddit.com/r/tlaplus/

nickpsecurity 8y ago
"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" Most evidence indicates using familiar concepts aids learning. That makes me hypothesize the best recommendation is the more mathematical ones for folks strong in math and the programmer-centric ones for those strong in that. That also implies that, for each of these formal topics, we need one version for each audience to draw more people in.
- fizwhiz 8y ago
  Seem's like hillel's material is more approachable for people with a programming background, and pron's recommended material better for people who are more math-y. I'm likely going to start with Hillel's books to develop a working understanding and then move onto Lamport's stuff once i'm ready for a rigorous deep dive.
fizwhiz 8y ago
This a great wealth of resources, thank you! Off-topic: from your linked videos, this video at the 2min 49s mark had me absolutely creased lmao http://video.ch9.ms/ch9/bab3/13798ec2-8479-4062-8aaf-94215670bab3/init2.mp4 http://video.ch9.ms/ch9/bab3/13798ec2-8479-4062-8aaf-9421567...

hwayne 8y ago

In my workshops people usually start being able to apply it to their business problems by about day 3. It's actually pretty simple once you get the hang of it! After those two, I'd probably recommend the original _Specifying Systems_. It can be a tough read, but it's a comprehensive dive into how TLA+ works mathematically and everything that you can do with it. You can get it for free here: https://lamport.azurewebsites.net/tla/book.html https://lamport.azurewebsites.net/tla/book.html I'd also recommend practicing by applying it to problems you've already solved in your place of work. That way you can compare it against a real system you know inside and out. I talk more about that here: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/ Does that answer your question?

fizwhiz 8y ago
Sure does, thank you!