The Future of TLA+ [pdf]

The Future of TLA+ [pdf]
lamport.azurewebsites.net

- It cannot compile to working code

- Steep learning curve

Opportunities for TLA+

- Helps you understand complex abstractions & systems clearly.

- It's extremely effective at communicating the components that make up a system with others.

Let get give you a real practical example.

In the AI models there is this component called a "Transformer". It under pins ChatGPT (the "T" in ChatGPT).

If you are to read the 2018 Transfomer paper "Attention is all you need".

They use human language, diagrams, and mathematics to describe their idea.

However if your try to build you own "Transformer" using that paper as your only resource your going to struggle interpreting what they are saying to get working code.

Even if you get the code working, how sure are you that what you have created is EXACTLY what the authors are talking about?

English is too verbose, diagrams are open to interpretation & mathematics is too ambiguous/abstract. And already written code is too dense.

TLA+ is a notation that tends to be used to "specify systems".

In TLA+ everything is a defined in terms of a state machine. Hardware, software algorithms, consensus algorithms (paxos, raft etc).

So why TLA+?

If something is "specified" in TLA+;

- You know exactly what it is — just by interpreting the TLA+ spec

- If you have an idea to communicate. TLA+ literate people can understand exactly what your talking about.

- You can find bugs in an algorithms, hardware, proceseses just by modeling them in TLA+. So before building Hardware or software you can check it's validity & fix flaws in its design before committing expensive resources only to subsequently find issues in production.

Is TLA+ simple? I find this hard to accept.

> TLA+ isn’t a programming language; it’s mathematics.

Mathematics is not executable, though, whereas TLA+ is.

> TLA+ [is better] for its purpose than a programming language.

"TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior."

"specification of system behavior" sounds like a programming language to me. A systems programming language, even.

All this is to say that it seems TLA+ really has no future. If there was a future, like a goal or a roadmap or something, it would be outlined in this document a lot more clearly - whereas, instead, it is more like "nope, everything's good, no changes needed", even as the language appears nowhere on the TIOBE rankings.