Thoughts on "The Future of TLA+"

What could be added to TLA+ without compromising Lamport's vision?

Last week Leslie Lamport posted The Future of TLA+, saying "the future of TLA+ is in the hands of the TLA+ foundation". Lamport released TLA+ in 1999 and shepherded its development for the past 25 years. Transferring ownership of TLA+ to the official foundation has been in the works for a while now, and now it's time.

In the document, Lamport also talks about some of his hopes for how the foundation will think about evolving TLA+. He gives three possible costs of any change:

1. Breaking existing specifications
2. Complicating the language. "Simplicity is a major goal of TLA+".
3. Complicating the tooling. "There are few people contributing to the maintenance of the tools."

With this, Lamport proposes removing several features, like octal numbers, submodules and tuple quantification.¹

I would be sad if we lost tuple quantification, less so if we lost octal numbers. But what could be added to make TLA+ better? Features that don't just "save a few keystrokes" but significantly prove the expressiveness of our specifications.

Some disclaimers. First, where I'm coming from: most of my contracts are either "get beginners started with TLA+" or "help a company write an exotic spec at the limit of what TLA+ can do." So I'm always thinking about how to teach the language better and how to abuse its most obscure features. Did you know about labeled subexpressions? You can do magic with labeled subexpressions.

So I both want the skill floor lowered and the skill ceiling raised. This is often a contradictory goal.

Second, these aren't official proposals or anything. I'm just sharing what I'd like to see, given infinite resources and no concerns about tradeoffs.

Finally, most of these aren't changes to TLA+. They're for TLC.

TLA+ vs TLC

TLA+ is the specification language. TLC is the model checker used to check that specs written in that language satisfy certain properties. It's not the only tool; you could use TLAPS or Apalache instead. But TLC is the most mature tool and the only one bundled with the standard distribution.

This is a critical distinction for two reasons. One, TLC can only model-check a subset of TLA+. There are a set of four "forbidden operators" that cannot be used in any capacity (though the lead TLC developer [Markus Kuppe] is working on adding one). Lamport lists them in section 3.3 of his essay.

Two, TLC makes some decisions about how to resolve some unspecified TLA+ operations. For example, CHOOSE x \in set: P(x) is undefined if no value in set satisfies P (Specifying Systems pg 73). In TLC, it's an error:

Attempted to compute the value of an expression of form
CHOOSE x in S: P, but no element of S satisfied P.

This catches a lot of design bugs where you expected something to exist but it doesn't. But it also makes specifying defaults awkward. What if I want to get the record with a certain id, but if there isn't one, return a default value NoRecord? Then I have to write this:

RetrieveRecord(id) ==
    IF \E r \in records: r.id = id
    THEN CHOOSE r \in records: r.id = id
    ELSE NoRecord

If the condition is longer, this gets more cumbersome, and there's always a risk of them getting out of sync.

The upside of TLC being separate from TLA+ is that we can add features to TLC without changing the overall semantics of TLA+. That's what Markus is doing in the TLC module: things like TLCGet and Assert adds new features to model checking TLA+ without adding new syntax to TLA+. It should be possible to make a new operator Try(Op, Fail) that evaluates Op and, if it fails, returns Fail instead. Then we can just do

RetrieveRecord(id) ==
    Try(CHOOSE r \in records: r.id = id, NoRecord)

With that in mind, most of the things I want in TLA+ are actually things I want in TLC, with one exception.

Things I wished were in TLA+/TLC

Try(Op, Fail)

It'd also be nice for equality checking. Right now "2" = 2 raises an error, even if I want it to be false.

(Could nested Trys lead to ambiguous behavior? Something to think about.)

A more obvious set filtering

This is the only change here that would affect TLA+ itself and not just TLC. This is map and filter in TLA+:

\* Map
{M(x): x \in set}
\* Filter
{x \in set: F(x)}

Beginners can never remember which is which. Even experienced people often forget which is which! I'd like a different keyword for each, so we could instead write

\* Filter
{x \in set WHERE F(x)}
\* Mapfilter
{M(x): x \in set WHERE F(x)}

Actual keyword may vary.

A linter

In the past few years TLA+ tooling has gotten a lot better. Among other things, there's now a debugger, a treesitter plugin, and an interactive spec explorer. I hope we soon see a linter, something that could detect TLA+ snippets with valid-but-unexpected behavior. In particular, something that could detect this:

/\ A
/\ B
 => C

That extra space before => means its parsed as A /\ (B => C), not as the expected (A /\ B) => C. I once lost a day to this. I know at least three other people who also lost a day to this. It is 100% valid TLA+ and we desperately need a tool to tell us when it happens because my gosh is it a morale-killer.

Support for the forbidden operators

There are four operators that are unsupported by TLC and virtually unused in any specs: \cdot, \EE, \AA, and -+->. I have no idea how to use \cdot but Markus is steadily adding support for it. \AA exists for completeness and even Lamport can't think of a good use for it. -+-> could be useful (It's the LTL weak release), but nobody's paid it any attention.

\EE is the interesting one, in that we know exactly how useful it would be. \EE x: P(x) is the temporal quantifier and is defined as "there exists a sequence of xs that make the temporal formula P(x) true for every step of the behavior. Critically, x can be a different value in each step, whereas \E x: P(x) would require the same value in each step.

Why is this so important? One word: refinement.

Say we have an abstract server model and we want make a more detailed version of just the server. We can refine it by instantiating the abstract spec like this:

Abstract == INSTANCE AbstractServer 
    WITH abstract_var1 <- formula1,
         abstract_var2 <- formula2,
         \* ...

Refinement == Abstract!Spec

See the above link for more details. The trouble is that we need to apply substitutions for every variable. If the abstract spec models both the server and the client, our refinement also needs to refine the client state, too! And more frustratingly, if the abstract spec has some kind of bookkeeping variable, say a state-sweeper or auxiliary variable, you have to refine that, too.

But TLA+ provides an out here. Using \EE, we can write the refinement like this:

Abstract(aux_var, client_var) == INSTANCE AbstractServer 
    WITH abstract_var1 <- formula1,
         abstract_var2 <- formula2,
         \* ...

Refinement == \EE a, c: Abstract(a, c)!Spec

Lamport calls this variable hiding (SS pg 41).

Now I don't know much about the internals of TLC, but my best guess is that \EE would be extraordinarily expensive to check. I think a regular refinement you can check as you go, since you can generate the full abstract transition at the same time you generate the main spec's transition. But with variable hiding, you only have information to create part of the abstract transition. I think the only way to do it would be to generate the abstract state graph first and then look for a transition that matches your current transition.

That is at the very least an NP-Complete problem, one you have to compute for every edge in your refinement graph. But maybe there are some special cases (like aux variables that do not affect behavior) which would be cheaper to check?

\E-stealing

This one's both the most niche and probably the hardest to implement, so I don't expect to see it anytime soon. But this is my newsletter and it bothers me specifically.

In Composing TLA+ Specifications with State Machines I used this trick to compose two specs:

Action1 ==
    /\ state = "start"
    /\ DoThing
    /\ state' = "wait"

Sync ==
    LET i == << state, state' >> IN
    CASE i == << "start", "wait" >> ->
        SomeSyncRules
      [] << "wait, start" >> ->
        DifferentSyncRules

So far, so good. But what if I take a nondeterministic action?

Action2 ==
    /\ state = "wait"
    /\ \E x \in set:
        DoThing(x)
    /\ state' = "start"


Sync ==
    LET i == << state, state' >> IN
    CASE i == << "start", "wait" >> ->
        SomeSyncRules
      [] << "wait, start" >> ->
        ???

There's no way for the body of Sync to know which value Action2 picked for x. I've found Sync actions are a great way to compose specifications, and this "opaqueness" limits how strong it can be. It'd be great to have some way of side-channeling out what x was picked, without changing the essential semantics of Action2. Preferably without even needing to modify it.

This might also be useful for test case generation, since you can augment the output traces with more information.

I have no idea what this would look like or how it would behave. It's just a pipe dream of mine.

Other pipe dreams

A better function update syntax. Some way to partially refine one spec into multiple, seamlessly upgrading their individual variables into function variables (without too much boilerplate). Being able to inline a config file in a spec so you don't need two separate files.[^inlining] Being able to call tlc without a config file and passing in flags. Support for -+->, just for giggles. Clock variables. Non-latex ASCII syntax. UNCHANGED (all vars except <>). Parallelized liveness checking. A tree that grants all my wishes.

[^inlining]: This is now provisionally possible! You can see an example here, run it with tlc -config Github866.tla Github866.tla

Comment Section

Buttondown now has comments! I'm experimentally enabling it for now, so you should be able to comment on the email's archive page. Again, this is experimental. If I end up having to spend all my time community moderating, comments are going down again. Be nice to each other.

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.