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 this, 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.
Re a more familiar syntax with the same TLA semantics, there is Quint, which also adds an excitability requirement which I think is a great idea in practice.
Re adding dependent types, +1 on avoiding that. A simple type system should suffice. Quint also adds something along those lines.
For as-you-type translation, plugins exist for neovim and emacs. Nobody has yet written one for VS Code (volunteers wanted!). TLAPM also does not yet support Unicode but I’m (slowly) working on this.
I know next to nothing about formal verification, so this is a naive question:
Once you’ve made a specification in one of these languages and proven various properties, are you then supposed to prove that your implementation matches that spec? If so, how?
Depends on the language. Right now, with TLA+, the most promising avenue so far has been to take the specification and generate a set of tests. See here: https://arxiv.org/abs/2006.00915
With other languages, it’s possible to generate code directly from the spec, but this comes at the cost of making the spec way harder to write.
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.
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.
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).
I do think this is right, though.
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.
Yes, please! Lean has this, 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.
Re a more familiar syntax with the same TLA semantics, there is Quint, which also adds an excitability requirement which I think is a great idea in practice.
Re adding dependent types, +1 on avoiding that. A simple type system should suffice. Quint also adds something along those lines.
Unicode support was merged into the Java tools this spring, so if you can input it, it will parse and be model-checked: https://ahelwer.ca/post/2024-05-28-tla-unicode/
An alignment-preserving unicode/ASCII translator utility exists: https://github.com/tlaplus-community/tlauc
For as-you-type translation, plugins exist for neovim and emacs. Nobody has yet written one for VS Code (volunteers wanted!). TLAPM also does not yet support Unicode but I’m (slowly) working on this.
The overall status of Unicode integration is tracked here: https://github.com/tlaplus/tlaplus-standard/tree/main/unicode#current-status
Cool! By the way, thanks for all your work on the TLA+ ecosystem.
I know next to nothing about formal verification, so this is a naive question:
Once you’ve made a specification in one of these languages and proven various properties, are you then supposed to prove that your implementation matches that spec? If so, how?
Depends on the language. Right now, with TLA+, the most promising avenue so far has been to take the specification and generate a set of tests. See here: https://arxiv.org/abs/2006.00915
With other languages, it’s possible to generate code directly from the spec, but this comes at the cost of making the spec way harder to write.