3 ms·

First of all, as always, huge respect for your work, and I'm looking forward to reading the rest of the posts. There is something I'd like to start a discussion

by hwayne 9y ago

First of all, as always, huge respect for your work, and I'm looking forward to reading the rest of the posts. There is something I'd like to start a discussion on, though: > nor will reading these posts teach you how to write good specifications; so this series is neither necessary nor sufficient for putting TLA+ to good use, but I think it is both necessary and sufficient for understanding it. Emphasis on the 'good specifications' part: I think this is a _huge_ oversight in the TLA+ community and the biggest barrier to its current adoption. The problem isn't that people don't understand (or can't understand) the theory behind it, yet it's the thing everybody focuses on teaching. The problem is specification: _nobody_ is talking about how to actually use TLA+. In fact, some of the advice given is actively harmful! One example: in _Specifying Systems_, Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. I find it telling that the majority of example TLA+ specs "in the wild" are either abstract algorithms or optimization problems. The things you don't find? How to write good invariants. When you should be using raw TLA+ versus the PlusCal syntax. Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier.

pron 9y ago
This is precisely the kind of discussion I want to see on the mailing list or /r/tlaplus. HN is not very conducive to internal community discussions.
pron 9y ago
> The problem is specification: _nobody_ is talking about how to actually use TLA+. I think that is Lamport's focus; he talks about this more than he talks about the theory. Plus, you have the Dr. TLA+ series. > Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. You definitely should write `NoVal == CHOOSE v : v \notin Val` in your spec (as that clarifies the intent) and override it as a "model value" (i.e., a constant) in TLC. This is best practice. Even `∃ x ∈ Nat` is not checkable by TLC, yet best practice is to leave it like that (as that is the intent), and override `Nat` in TLC. In either case, the more general specification is verifiable in TLAPS. > Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. This kind of discussion is very common on the mailing list (there are a lot of hidden gems there), but I would be very happy to see more people write "pro tips" and publishing them. > Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier. My personal goal in this particular series is just to get people interested in the theory. But TLA+ is still extremely young when it comes to "use in the wild". It was virtually nonexistent before 2012, and started slowly gaining traction only around 2014, when Amazon published their report. As you can see, writing short and to the point tips, tricks and guides isn't exactly my forté, but they are extremely important. As this tiny community grows, there will hopefully be those that will fill in the missing gaps. Your own tutorial is a great start.

by hwayne 9y ago

pron 9y ago

This is precisely the kind of discussion I want to see on the mailing list or /r/tlaplus. HN is not very conducive to internal community discussions.

pron 9y ago

> The problem is specification: _nobody_ is talking about how to actually use TLA+. I think that is Lamport's focus; he talks about this more than he talks about the theory. Plus, you have the Dr. TLA+ series. > Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. You definitely should write `NoVal == CHOOSE v : v \notin Val` in your spec (as that clarifies the intent) and override it as a "model value" (i.e., a constant) in TLC. This is best practice. Even `∃ x ∈ Nat` is not checkable by TLC, yet best practice is to leave it like that (as that is the intent), and override `Nat` in TLC. In either case, the more general specification is verifiable in TLAPS. > Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. This kind of discussion is very common on the mailing list (there are a lot of hidden gems there), but I would be very happy to see more people write "pro tips" and publishing them. > Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier. My personal goal in this particular series is just to get people interested in the theory. But TLA+ is still extremely young when it comes to "use in the wild". It was virtually nonexistent before 2012, and started slowly gaining traction only around 2014, when Amazon published their report. As you can see, writing short and to the point tips, tricks and guides isn't exactly my forté, but they are extremely important. As this tiny community grows, there will hopefully be those that will fill in the missing gaps. Your own tutorial is a great start.