The Future of TLA+ [pdf]

There's very little tech that somebody is going to hire you for knowing. It's a tool like many others.

If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.

Every time I see a new TLA+ replacement my first thought is "Oooh this will be good for the 99% of normal stuff people do with TLA+."

Then I look through some of the specs I've written with clients and find the one absolutely insane thing I did in TLA+ that would be impossible in that replacement.

Shoutout to operator labels.

> Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages.

Yeah, but in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Programming languages of every generation are very useful, as is mathematics, even though they're not the same thing.

> More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases.

Coq and Idris are very different in the way they're typically used, and I'd say TLA+ is much closer to Coq than to Idris (and is probably more popular than the two combined), but to "execute" anything the specification needs to be at a certain level that's detailed enough to produce a program, and oftentimes that is very much not what you want.

It would be extremely useful to have a language that you could describe the various properties of a car and it would compile your specification into the design of a car (you would need to give it sufficient detail as there are choices to be made). But it would also be extremely useful to have a language that could be used to learn certain things about a car -- say, it's braking distance -- without specifying it in sufficient detail to actually build one. That is what maths is good for -- describing things at arbitrary levels of detail to answer relevant questions.

For example, you may have a 5 MLOC distributed system, and you want to know if a certain kind of failure may lead to data loss. You could use TLA+ to describe just the relevant details to answer the question in, say, 200 lines of formulas. That you cannot compile those formulas into a working 5 MLOC piece of software is not a downside of mathematics, but rather the point.

> TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be

And because it's not a language for programming but a language for mathematics, so it looks and feels pretty close to plain mathematics (only it's formal), as that's the obvious choice for writing mathematics.

I may have been spending too much time with Lean recently, but the number one thing I’d like to see for the future of TLA+ is an equivalent of Mathlib (https://github.com/leanprover-community/mathlib4). What’s so great about the experience of using Lean is that I can pull theorems off the shelf from Mathlib, use them if I want to, or learn from the way their proofs work if I want to do something similar.

> The reason for using TLA+ is that it isn’t a programming language; it’s mathematics.

I love TLA+, I’ve used it for a decade and reach for it often. I have a huge amount of respect for Leslie Lamport and Chris Newcombe. But I think they’re missing something major here. The sematics of TLA+ are, in my mind, a great set of choices for a whole wide range of systems work. The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language (and, in particular, translate other ways of expressing mathematics into TLA+).

I would love to see somebody who thinks deeply about PL syntax to make another language with the same semantics as TLA+, the same goals of looking like mathematics, but more familiar syntax. I don’t know what that would look like, but I’d love to see it.

It seems like with the right library (see my mathlib point) and syntax, writing a TLA+ program should be no harder than writing a P program for the same behavior, but that’s not where we are right now.

> The errors [types] catch are almost always quickly found by model checking.

This hasn’t been my experience, and in fact a lot of the TLA+ programs I see contain partial implementations of arbitrary type checkers. I don’t think TLA+ needs a type system like Coq’s or Lean’s or Haskell’s, but I do think that some level of type enforcement would help avoid whole classes of common specification bugs (or even auto-generation of a type checking specification, which may be the way to go).

> [A Coq-like type system] would put TLA+ beyond the ability of so many potential users that no proposal to add them should be taken seriously.

I do think this is right, though.

> This may turn out to be unnecessary if provers become smarter, which should be possible with the use of AI.

Almost definitely will. This just seems like a no-brainer to bet on at this stage. See AlphaProof, moogle.ai, and many other similar examples.

> A Unicode representation that can be automatically converted to the ascii version is the best alternative for now.

Yes, please! Lean has a unicode representation, along with a nice UI for adding the Unicode operators in VSCode, and it’s awesome. The ASCII encoding is still something I trip over in TLA+, even after a decade of using it.

Whoa, I use TLA ironically to joke about Three Letter Acronyms, I had no idea that the Three Letter Acronym (TLA) was in any way related to Temporal Logic Actually. Fascinating!