by tkhattra on 8/28/24, 6:46 PM with 105 comments
by mjb on 8/28/24, 11:20 PM
> 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.
by hwayne on 8/28/24, 9:47 PM
There's another reason to potentially support \EE: it's needed to refine specs with auxiliary variables. Currently, if an abstract spec has `aux_hist` to prove a property or something, you need the refinement to have an `aux_hist` equivalent, even if it doesn't affect the spec behavior at all. But if checkers could handle `\EE` you could instead leave it out of the refinement and check `\EE aux_hist: Abstract(aux_hist)!Spec`.
I think /u/pron once told me that actually checking a property of that form is 2-EXPTIME complete, though. Which is why it's not supported in practice.
by rtpg on 8/28/24, 11:44 PM
Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling?
(Aside: I have a TLA+ book, but it's notably missing really much in terms of exercises or anything. If anyone has any recommendations for a large set of exercises to play around in the space I'd love to hear about it!)
EDIT: turns out just searching for "temporal logic in X language" gets you papers, found this one paper for axiomatizing temporal logic that seems to be a good starting point for anyone looking at this [0]
[0]: https://lim.univ-reunion.fr/staff/fred/Enseignement/Verif-M2...
by bokumo on 8/28/24, 7:33 PM
by wizerno on 8/28/24, 9:30 PM
TLA+ isn't taught in most universities and while I've read about so many interesting applications, I'm yet to convince myself that someone would hire me for knowing it rather than just teaching it to me on the job. Any tips to get started would also be appreciated!
by pnathan on 8/29/24, 1:10 AM
I did not find it straight forwardly grokkable, which makes me sad. Maybe it needs a library of axioms? I feel there's probably a very nice way to work through it without ingesting effectively a graduate school course in proving software.
It really is just math and proofs, it shouldn't be so hard... to start.
Well, that's my take. Could be wrong. Might just need to hit the books.
by threatofrain on 8/28/24, 7:09 PM
by fat_cantor on 8/28/24, 11:37 PM
by jayaprabhakar on 8/30/24, 3:42 AM
by penguin_booze on 8/29/24, 7:12 PM
I bet you a million dollars [0] that Mr. Lamport absolutely is the sole author of this sentence.
[0] which I don't have. You may resume reading.
by Mathnerd314 on 8/28/24, 8:10 PM
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.