Fifteen days left
Hi everyone! Been a couple of weeks since the last email. As mentioned, I took June off from weekly newsletter to work on the new version of the learntla web site. I have a requirement to have a version I’m happy uploading by the end of June, or else I owe a random one of you a thousand dollars. That’s just two weeks away, and I figure I should update everyone on how that’s coming so far.
Currently I’ve written about 28,000 words. That’s about twice the current version of learntla and about half the length of Practical TLA+. With the exception of the sections on Action Properties and pure TLA+, all of the core learning material is in “polish mode”. Action Props are about 60% done, pure TLA+ is maybe 30% done. I also need to take a lot more screenshots and make a lot more diagrams— dreary work, but easy enough to do.
In addition to core material, I’m writing a bunch of special topic essays. Here’s the stuff I want in the MVP:
- General Tips on how to write better TLA+.
- Using the Toolbox: configuration options, trace explorer, profiler, misc features.
- Beyond the Toolbox: how to configure and run TLA+ from the command line.
- Auxiliary variables: Ways of augmenting a spec with bookkeeping data to get more information.
- State Machines: PlusCal and TLA+ representations of SMs, TLA+ representations of hierarchical state machines.
- Refinement: Basically a copy of this article.
Some topics notably missing from the MVP: model optimization, the standard library, community modules, complex temporal properties, modeling legacy systems, or fitting TLA+ into a team setting. These are all things that I plan to write. The big reason I’m rewriting learntla from ground up (aside from getting to use Sphinx for documenting) is so I can make it a central location for all my TLA+ material. Right now I have to put new techniques on my blog, which isn’t great for discoverability.
I’m splitting examples into three subcategories:
- Examples of writing complex operators
- Examples of PlusCal specifications
- Examples of pure TLA+ specifications.
Right now I only have one example written, a copy of my golang article. I might add a few more operator examples by the end of the month, but it’ll be shallow on spec examples for a while.
Technical Stuff
Rewriting the whole thing in Sphinx continues to pay dividends. Check out this awesome index page!
God I love Sphinx so much. I get why it’s unpopular (a lot harder to use than easy markdown site generators), but the power ceiling is so dang high
TLA+ Conference
Speaking of TLA+, we have a conference this September! It’s colocated with Strange Loop, so if you’re going to that why not check us out too? I’ll be running the official workshop on Sept 21st. Come join me, it’ll be fun!