4 ms·

How should I get started with TLA+? I don’t have any experience.

Jtsummers 6y ago
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/ https://learntla.com/introduction/ [1] https://lamport.azurewebsites.net/tla/learning.html https://lamport.azurewebsites.net/tla/learning.html
- gralx 6y ago
  I would add an excellent introduction by Scott Wlaschin on YouTube called "Building confidence in concurrent code using a model checker."[0] Lamport's Specifying Systems (2002, linked above) is a great book. It covers ground quickly but has deep roots - you can tell Lamport is an expert logician who engineered the language carefully. I recommend you read the first two chapters of that (free) book before you do anything else, but you may feel like you're wading through mud if you don't start writing simple specs and watch his or other tutorials by chapter 5. Most of his example specifications (Chapter 5, Chapter 11) design a memory interface for a computer, and they suppose you are familiar with basic computer architecture. If not, you'll have to learn TLA+ while learning how a memory interface works at the same time, which takes dedication. The appeal to me of TLA+ is using set theory and first-order predicate logic to describe any system, from a poker game to a shopping trip to a computer program - anything at all where the next state depends on the history of the system after a set of initial states. The TLA+ Toolbox IDE has a TLA+ model checker called TLC that can test your logic, and that is particularly useful for a complex concurrent or distributed system if you ever design one. [0] https://www.youtube.com/watch?v=tqwcz-Yt9gQ https://www.youtube.com/watch?v=tqwcz-Yt9gQ
berlinquin 6y ago
I can second Lamport's series of video lectures. I worked through them recently and found the teaching and the examples to work through very engaging.

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/ https://learntla.com/introduction/ [1] https://lamport.azurewebsites.net/tla/learning.html https://lamport.azurewebsites.net/tla/learning.html

gralx 6y ago
I would add an excellent introduction by Scott Wlaschin on YouTube called "Building confidence in concurrent code using a model checker."[0] Lamport's Specifying Systems (2002, linked above) is a great book. It covers ground quickly but has deep roots - you can tell Lamport is an expert logician who engineered the language carefully. I recommend you read the first two chapters of that (free) book before you do anything else, but you may feel like you're wading through mud if you don't start writing simple specs and watch his or other tutorials by chapter 5. Most of his example specifications (Chapter 5, Chapter 11) design a memory interface for a computer, and they suppose you are familiar with basic computer architecture. If not, you'll have to learn TLA+ while learning how a memory interface works at the same time, which takes dedication. The appeal to me of TLA+ is using set theory and first-order predicate logic to describe any system, from a poker game to a shopping trip to a computer program - anything at all where the next state depends on the history of the system after a set of initial states. The TLA+ Toolbox IDE has a TLA+ model checker called TLC that can test your logic, and that is particularly useful for a complex concurrent or distributed system if you ever design one. [0] https://www.youtube.com/watch?v=tqwcz-Yt9gQ https://www.youtube.com/watch?v=tqwcz-Yt9gQ

berlinquin 6y ago

I can second Lamport's series of video lectures. I worked through them recently and found the teaching and the examples to work through very engaging.