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.
I loved the concept of TLA+ and tried to get into it, but as you say
> The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language
the syntax was very non-standard which was off putting, and the expected dev ux seemed to be of the 'get it right on paper first then just write the text' variety. This was also off putting and I think you're right that there is a space for making a DX focused TLA+ transpiled language
> 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.