Leslie Lamport has a video course[0] on TLA+ that's slowly being released. I created an RSS feed[1] that updates as new episods are released.<p>[0] <a href="https://lamport.azurewebsites.net/video/videos.html" rel="nofollow">https://lamport.azurewebsites.net/video/videos.html</a><p>[1] <a href="http://fetchrss.com/rss/58d198538a93f8ef3b8b4567741573560.atom" rel="nofollow">http://fetchrss.com/rss/58d198538a93f8ef3b8b4567741573560.at...</a>
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:<p>> 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.<p>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 <i></i>use<i></i> TLA+. In fact, some of the advice given is actively harmful!<p>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+.<p>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.<p>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.
Very nice. I really appreciate you placing TLA+ in context with alternate approaches. I look forward to seeing the followup posts.<p>PS: How are you generating these pages? Jekyll? something else?<p>EDIT: This probably needs editing -- "nor will reading the posts will not teach you how to write good specifications;"<p>I <i>think</i> you probably meant to write "nor will reading the posts teach you how to write good specifications;"
@ pron<p>This is a great write-up I learn quite a bit from but way, way, too long. There's a lot of redundancy in here much like my first sentence. You should try to condense this since the redundancy might make a chunk of the modern crowd think the rest of what they see in the scrollbar will be the same and move on to next article. The last write-up you sent me didn't have that problem.<p>I'm glad I saw this, too, as I recently watched your video citing all the mathematical evidence that correctness may not decompose. I got one or two counterpoints to email you later but overall want your data peer reviewed by people highly experienced in abstractions in large, verification efforts and making VCG's given their output will have to compose, too. Let all the pro's duke it out with arguments, proofs, and attempts at actual projects. I'll reserve judgment until the dust settles. :)
Great article, and I look forward to the next! I've been meaning to learn about TLA+ for a while.<p>One thought I didn't see expressed, in all the comparisons of tools and approaches, is that sometimes you don't care about time and state. In purely "transformational" programs, like compilers, for example, all state is incidental complexity, so we can analyze them as pure functions. Meanwhile, all the questions such as whether we can just execute the spec and whether we can prove properties of real programs remain. New web frameworks are trying to keep the parts that deal with time and state as small and self-contained as possible, leaving the rest to be described using functions.<p>Couldn't we say that the factor of "do you care about time" is behind observations such as that TLA+ is mostly popular with concurrent and distributed systems, or that approaches that only look at function contracts often apply to pieces of a program but not the whole? As a more specific statement than, for example, that distributed systems are particularly hard so they necessitate particularly powerful tools.