Update on Learntla and a new writing process

Hey everyone!

I realize I should give you all an update on the current learntla progress! So first of all, I've been continuously pushing my work to the learntla-v2 repo. Every push also builds the virtualenv as the artifact, so if you want to see the current state of the documentation, you can clone the repo, download the venv, and then run venv/bin/sphinx-build to get a local copy.

Currently I'm 15,000 words in and expect to have the first public version ready by the end of June. To keep myself to that schedule I set up a toxx clause: If I miss the deadline I'll pay $1000 to a random newsletter subscriber. That public version won't be the intended final version, just the minimal content I'd be happy with. In particular, to cut scope I'm leaving out all exercises.

v2 is organized slightly differently from v1 and Practical TLA+. In addition to reordering the content (constants now come much earlier, and nondeterminism comes after functions), I'm splitting examples up into simple "in-band" ones that are inline with the teaching material and complex "out-of-band" ones that are on separate (linked) pages. That way I can separate "examples for showing the concepts in use" from "examples for learning how to specify better". Also, I reuse the same problem for the in-band examples. Currently, the two main in-band examples are "checking if a string contains duplicates" and "threads incrementing a counter", though there are a couple others, too. The out-of-band examples are going to be more diverse. None of those are written yet, but the ones I plan to do are (at the very least):

1. My goroutines spec rewritten as an instructional example
2. The thread scheduler spec
3. Adversarial nondeterminism (as a tictactoe "AI")
4. A distributed duplicates checker

The main new content expansion will be about writing TLA+ without PlusCal. I'm going to explain it by comparing predictable PlusCal specs to their TLA+ translations and discussing how each PlusCal "feature" is emulated in the TLA+ layer. Other planned content: how to optimize model checking, how to use TLA+ from the command line, advanced techniques like refinement, the community models.

Tech Updates

Every time I write a new resource, I try a bunch of new teaching ideas to see which work. I experiment with both the kinds of content I write and the tech I use to present it.

Content experiments: Going to be presenting more "war stories". Normally I like making every spec a fully self-contained example. The problem is that keeping specs simple enough to be self-contained in a chapter makes them less interesting. Now I'm also giving parts of specs that I've written for work. Here's one bit from the functions chapter:

Why functions over operators? We rarely use functions for computations— operators are far superior for that. Functions are important as values. We can assign them to variables and manipulate them like any other value.

In a spec I once wrote, I had to assign tasks to CPUs. Some tasks needed to be assigned to many CPUs, but each CPU should only have one task. In that spec, the best solution was to store assignments as functions, where each task mapped to a set of CPUs.

  variables
    assignments = [t \in Tasks |-> {}]

Then I could write assignment[t] := assignment[t] \union {cpu} to assign cpu to task t. For my invariant, I said no two tasks shared a CPU assignment.

 OnlyOneTaskPerCpu ==
   \A t1, t2 \in Tasks, c \in CPU:
     /\ (t1 # t2) 
     /\ c \in assignments[t1] 
     => c \notin assignments[t2]

So I'm not providing the entire spec I wrote, because that would be too confusing for the reader. But it'll still be more interesting.

Techwise I'm pushing hard on using semantic text for writing documentation. All my earlier TLA+ material was in Markdown, which I've had many, many problems with. I tried semantic text for the Alloydocs and it really helped; this is now my most serious attempt. And so far, it's paying off! It makes maintaining the content easier, and I also hope it'll present better content.

The best demo of maintaining content is the spec directive I wrote. I can now write this:

To allow users to also subtract and multiply, we can place the addition logic in an ``either`` branch, and then create two more branches.

.. spec:: calculator/2/calculator.tla
  :diff: calculator/1/calculator.tla

And get this:

The directive automatically finds the files, produces the diff between the specs, removes the unsightly filenames from the top of the diff, and adds a link to the full spec if you want to just copy and paste instead of typing in all the changes yourself. Very clean.

I haven't done as much with semantic text for external-facing things, especially now that I'm leaving exercises out of the first public version. One idea I had is the troubleshooting tag: it renders the troubleshooting as normal text but also adds it to a troubleshootinglist. I intend to then make a "troubleshooting" page, which aggregates all of the tips I wrote throughout the entire guide. It sounds useful, but I don't know if it will be useful.

New Writing Process

I divide my writing into three categories:

1. Work commitments: freelance essays, upcoming talks, contracts, the weekly newsletter.
2. "Short-term" projects, which means the blog posts.
3. "Long-term" projects, like the Crossover Project, the Alloy docs, and learntla.

Early in the year I was overprioritizing short-term to the detriment of learntla, which is why I did a complete hiatus. Not only am I not publishing new blog posts, I'm not even writing them.¹ This has been good for getting the long-term project done but it went way too far and now I feel like my blog was too neglected. I had an idea for a new process to adopt after this is done, which I hope will be more balanced:

1. During long-term projects I'll keep writing blog posts, but only post them to a buffer (with a carveout for urgent posts, like the Alloy 6 writeup.)
2. I can only start pulling from the buffer after the project is done.
3. If the buffer ever runs out, I can't start writing new blog posts until I start a new long-term project.

I'll try this process for the next long-term project after the learntla and alloydoc updates, which I'll spoil now will be Hacker Test History. I've been telling myself I want to do it for four years now, and it's finally time, dammit

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.