The Future of TLA+ [pdf]

Original Article ↗ Hacker News Discussion ↗

What TLA+ Is (and Isn’t)

  • Repeated emphasis that TLA+ is a mathematical specification language, not a programming language.
  • Specs describe system behavior at arbitrary abstraction levels; many valid specs are not executable or even computable.
  • Users stress the value of being able to write short specs (hundreds of lines) for very large systems (millions of LOC) to answer questions like “can this fail in way X?”.

Specification vs Programming Debate

  • One side argues TLA+ behaves like a logic/programming language (similar to Prolog), since tools like TLC “run” specs and can even print or simulate behavior.
  • The counterargument:
    • TLA+ can express non-computable objects (e.g., a halting oracle, real-number properties), which by definition go beyond programming.
    • Tools (TLC, TLAPS, other checkers) operate on subsets of TLA+ and don’t define the language itself.
    • Spec languages differ from programming languages because they can say both what must happen and what must not happen and need not fix implementation choices.

Strengths and Limitations

  • Strengths:
    • Very good for concurrent and distributed systems, interleavings, and refinement reasoning.
    • Used successfully in industry (e.g., AWS paper cited) to catch subtle logical/design bugs.
    • Helpful for clarifying complex systems and communicating designs.
  • Limits:
    • Not suited to numerical/matrix-heavy algorithms like transformers; better for discrete state machines.
    • Poor at predicting emergent performance pathologies (feedback loops, sustained slowdowns).
    • Side channels and low-level hardware issues are out of scope.

Syntax, Tooling, and Alternatives

  • Many find the syntax “simple but not easy”: mathematically clean yet unfamiliar to programmers; temporal logic especially feels non-intuitive.
  • Critiques of tooling UX and ASCII encodings; desire for better Unicode support and IDE integration.
  • Interest in TLA+-inspired or TLA-based alternatives with more familiar syntax or closer-to-code feel (Quint, P, FizzBee).
  • Some see the lack of types as a gap; others say model checking usually catches type-like errors. Strong Coq/Lean-style types are seen as too heavy.

Learning, Adoption, and Ecosystem

  • TLA+ is rarely a hiring requirement; viewed as a powerful niche tool rather than mainstream tech.
  • Advice: treat it as one more tool, learn by small experiments, possibly via video courses or books.
  • Calls for more exercises, libraries (like Lean’s mathlib), and higher-level “DX-focused” layers to lower the entry barrier.