8 ms·

The Future of TLA+ [pdf]

195 points by tkhattra 2y ago

fat_cantor 2y ago
Whoa, I use TLA ironically to joke about Three Letter Acronyms, I had no idea that the Three Letter Acronym (TLA) was in any way related to Temporal Logic Actually. Fascinating!
threatofrain 2y ago
A TLA+ alternative people might find curious. https://quint-lang.org/ https://quint-lang.org/
- westurner 2y ago
  What are other limits and opportunities for TLA+ and similar tools?
  - max_ 2y ago
    Limits of TLA+ - 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.
    - skybrian 2y ago
      Is that a practical example? Has anyone specified a transformer using TLA+? More generally, is TLA+ practical for code that uses a lot of matrix multiplication?
      - drdrey 2y ago
        It’s really not, TLA+ works best for modeling state machines with few discrete states and concurrent systems. It can find interesting interleaving of events that would leave to a violation of your system properties
      - fiddlerwoaroof 2y ago
        The most practical examples I’m aware of are the usage of TLA+ to specify systems at AWS: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
        westurner 2y ago
        From "Use of Formal Methods at Amazon Web Services" (2014) https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... : > What Formal Specification Is Not Good For: We are concerned with two major classes of problems with large distributed systems: 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising ‘sustained emergent performance degradation’ of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don’t yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. We use other techniques to mitigate those risks. Delay, cycles, feedback; [complex] [adaptive] nonlinearity Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer. > This raised a challenge; how to convey the purpose and benefits of formal methods to an audience of software engineers? Engineers think in terms of debugging rather than ‘verification’, so we called the presentation “Debugging Designs” [8] . Continuing that metaphor, we have found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it: Exhaustively testable pseudo-code > We initially avoid the words ‘formal’, ‘verification’, and ‘proof’, due to the widespread view that formal methods are impractical. We also initially avoid mentioning what the acronym ‘TLA’ stands for, as doing so would give an incorrect impression of complexity. Isn't there a hello world with vector clocks tutorial? A simple, formally-verified hello world kernel module with each of the potential methods would be demonstrative, but then don't you need to model the kernel with abstract distributed concurrency primitives too? From https://news.ycombinator.com/item?id=40980370 https://news.ycombinator.com/item?id=40980370 ; > - [ ] DOC: learnxinyminutes for tlaplus > TLAplus: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B > awesome-tlaplus > Books, (University) courses teaching (with) TLA+: https://github.com/tlaplus/awesome-tlaplus#books https://github.com/tlaplus/awesome-tlaplus#books FizzBee, Nagini, deal-solver, z3, dafny; https://news.ycombinator.com/item?id=39904256#39938759 https://news.ycombinator.com/item?id=39904256#39938759 , "Industry forms consortium to drive adoption of Rust in safety-critical systems" (2024) https://news.ycombinator.com/item?id=40680722 https://news.ycombinator.com/item?id=40680722 awesome-safety-critical:
  - RandomThoughts3 2y ago
    Formal specifications benefits are clear and I think well understood at that point. If you want to ensure that your specifications is coherent and doesn’t have unexpected behaviour, having a formal specification is a must. It’s even a legal requirement for some system nowadays in safety critical applications. The issue of TLA+ is that it doesn’t come from the right side of the field. Most formal specifications tools were born out of necessity from the engineering fields requiring them. TLA+ is a computer science tool. It sometimes shows in the vocabulary used and in the way it is structured.
- lolinder 2y ago
  Previously discussed: https://news.ycombinator.com/item?id=41111790 https://news.ycombinator.com/item?id=41111790
- pron 2y ago
  I wouldn't say it's a TLA+ alternative because it cannot do the most powerful and useful things TLA+ does (esp. refinement), but it is an alternative for programmers who just want to specify at a level that closer to code and model-check specifications.
  - hwayne 2y ago
    Every time I see a new TLA+ replacement my first thought is "Oooh this will be good for the 99% of normal stuff people do with TLA+." Then I look through some of the specs I've written with clients and find the one absolutely insane thing I did in TLA+ that would be impossible in that replacement. Shoutout to operator labels.
    - setheron 2y ago
      So for us normies does that mean skip TLA?
      - hwayne 2y ago
        None of the replacements I've seen so far are mature enough for me to recommend them over TLA+.
        igornotarobot 2y ago
        I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago was probably an exception to that. The other companies wish to immediately hide these tools and the benchmarks behind the IP and closed source. As a result, we have early stage MVPs that are developed by 1-3 people.
- pnathan 2y ago
  I don't see any peer reviews of quint's work on their site or GitHub. Am I missing them?
  - igornotarobot 2y ago
    When you say peer reviews, do you mean academic publications or testimonials? I imagine it would be difficult to publish a paper at an academic conference proposing an alternative syntax for anything, even if it were better.
- bvrmn 2y ago
  It's kinda raw at this point of development. Could be a promising alternative for pluscal.
mjb 2y ago
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 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.
- vosper 2y ago
bokumo 2y ago
What LaTeX package does one use to get the "back" link at the end of footnotes like the linked PDF exhibits?
- gurjeet 2y ago
  Yes, that's an interesting implementation. I'm using Firefox, and the jumps to the notes and back to the paragraph are recorded in history, and has the expected effect when clicking the back and forward history arrows/buttons.
- evomassiny 2y ago
  hyperref does this with the "\ref{}" command, it can link to any defined \label
leogss27 2y ago
[flagged]
Mathnerd314 2y ago
> Simplicity is a major goal of TLA+. 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.
- colanderman 2y ago
  TLA+ is only "executable" in the same sense that an algebraic expression is executable. It's perfectly possible to write things on TLA+ that can not be simply executed linearly. (These overlap to a great extent with the things which TLC rejects.) As a basic example, it's easy to write a statement with \A (unbounded universal quantification) whose truth can only be judged by a proof engine. Specification languages are explicitly not programming languages, for the core reason that programming languages dictate only what must occur; whereas specification languages can dictate what must not occur. It's not possible with a "specification" written using a programming language to determine what of a program is actually the specification, vs. what is an accident of the implementation.
  - AlotOfReading 2y ago
    Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages. More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases. TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be, not because there's some universal line dividing specification languages from programming languages. It's also one of the biggest hurdles to TLA+ usage.
wizerno 2y ago
As someone who's fascinated by formal verification and who's early in their career, what advice do senior folks who have been using TLA+ have? 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!
- kadoban 2y ago
  There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.
  - mnk47 2y ago
    >There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. I guess this must be true on places like SF since I see this so often on HN, but almost every single job listing I've seen strictly requires knowledge of a specific tech stack, with the exception of a few internship programs.
    - Turfie 2y ago
      Exactly my thoughts as well.
    - kadoban 2y ago
      There's tech that if it's not on your resume, you won't pass the first filter. But that's different. Knowing it will _not_ get you a job, it'll just get you past some early step. But things like TLA+ are way different from even that. The number of programming jobs that will bin you if you don't have TLA+ on your resume has to be like, 5 in the world. Nobody is going to see it on there and be like "we _must_ hire this person!".
- SonOfLilit 2y ago
hwayne 2y ago
> The [\EE] operator is needed to explain the theory underlying how TLA+ is used. 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.
rtpg 2y ago
I'm really not a fan of TLA+'s tooling, but I do really love the temporal logic. I've always kinda wanted that stuff in other proving languages, but I don't know how possible it is. 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/Articles/An%20Axiomatization%20of%20Linear%20Temporal%20Logic%20in%20the%20Calculus%20of%20Inductive%20Constructions-Coupet-Grimal-2002.pdf https://lim.univ-reunion.fr/staff/fred/Enseignement/Verif-M2...
- zozbot234 2y ago
  > 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? Temporal logic is just a specific instance of a modal logic, which can be modeled with reasonable ease using a "possible worlds"-based encoding. Note that TLA+ combines temporal logic with non-determinism, which is a different modality.
pnathan 2y ago
I was looking at TLA a few months ago to consider what it would take to prove multiregion fail over worked correctly. Considering I'd never looked at it before. 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.
- mjb 2y ago
  I'd suggest starting with P (https://github.com/p-org/P https://github.com/p-org/P), or picking up Hillel Wayne's TLA+ book to get started.
  - sriram_malhar 2y ago
    P is very nice indeed, be advised that it is not an exhaustive checker like TLC (TLA+'s model checker, or Apalache, the symbolic tester). It is more like a higher-level testing framework. That said, since non-deterministic choices are equi-probable in P, failure conditions are triggered at much higher frequencies than in a conventional testing scenario.
- nektro 2y ago
  https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html is really excellent
penguin_booze 2y ago
> The superscript 1 at the end of this sentence is a link to an end note; click on it now. 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.
jayaprabhakar 2y ago
TLA+ is 25 years old. Despite the power it's syntax is too alien to become mainstream. Have you considered https://FizzBee.io https://FizzBee.io? Almost Python-like syntax, has more powerful semantics, beautiful visualizations with no extra work, only formal methods system that can do performance analysis.

195 points by tkhattra 2y ago

Whoa, I use TLA ironically to joke about Three Letter Acronyms, I had no idea that the Three Letter Acronym (TLA) was in any way related to Temporal Logic Actually. Fascinating!

threatofrain 2y ago

A TLA+ alternative people might find curious. https://quint-lang.org/ https://quint-lang.org/

westurner 2y ago
What are other limits and opportunities for TLA+ and similar tools?
- max_ 2y ago
  Limits of TLA+ - 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.
  - skybrian 2y ago
    Is that a practical example? Has anyone specified a transformer using TLA+? More generally, is TLA+ practical for code that uses a lot of matrix multiplication?
    - drdrey 2y ago
      It’s really not, TLA+ works best for modeling state machines with few discrete states and concurrent systems. It can find interesting interleaving of events that would leave to a violation of your system properties
    - fiddlerwoaroof 2y ago
      The most practical examples I’m aware of are the usage of TLA+ to specify systems at AWS: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
      - westurner 2y ago
        From "Use of Formal Methods at Amazon Web Services" (2014) https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... : > What Formal Specification Is Not Good For: We are concerned with two major classes of problems with large distributed systems: 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising ‘sustained emergent performance degradation’ of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don’t yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. We use other techniques to mitigate those risks. Delay, cycles, feedback; [complex] [adaptive] nonlinearity Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer. > This raised a challenge; how to convey the purpose and benefits of formal methods to an audience of software engineers? Engineers think in terms of debugging rather than ‘verification’, so we called the presentation “Debugging Designs” [8] . Continuing that metaphor, we have found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it: Exhaustively testable pseudo-code > We initially avoid the words ‘formal’, ‘verification’, and ‘proof’, due to the widespread view that formal methods are impractical. We also initially avoid mentioning what the acronym ‘TLA’ stands for, as doing so would give an incorrect impression of complexity. Isn't there a hello world with vector clocks tutorial? A simple, formally-verified hello world kernel module with each of the potential methods would be demonstrative, but then don't you need to model the kernel with abstract distributed concurrency primitives too? From https://news.ycombinator.com/item?id=40980370 https://news.ycombinator.com/item?id=40980370 ; > - [ ] DOC: learnxinyminutes for tlaplus > TLAplus: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B > awesome-tlaplus > Books, (University) courses teaching (with) TLA+: https://github.com/tlaplus/awesome-tlaplus#books https://github.com/tlaplus/awesome-tlaplus#books FizzBee, Nagini, deal-solver, z3, dafny; https://news.ycombinator.com/item?id=39904256#39938759 https://news.ycombinator.com/item?id=39904256#39938759 , "Industry forms consortium to drive adoption of Rust in safety-critical systems" (2024) https://news.ycombinator.com/item?id=40680722 https://news.ycombinator.com/item?id=40680722 awesome-safety-critical:
- RandomThoughts3 2y ago
  Formal specifications benefits are clear and I think well understood at that point. If you want to ensure that your specifications is coherent and doesn’t have unexpected behaviour, having a formal specification is a must. It’s even a legal requirement for some system nowadays in safety critical applications. The issue of TLA+ is that it doesn’t come from the right side of the field. Most formal specifications tools were born out of necessity from the engineering fields requiring them. TLA+ is a computer science tool. It sometimes shows in the vocabulary used and in the way it is structured.
lolinder 2y ago
Previously discussed: https://news.ycombinator.com/item?id=41111790 https://news.ycombinator.com/item?id=41111790
pron 2y ago
I wouldn't say it's a TLA+ alternative because it cannot do the most powerful and useful things TLA+ does (esp. refinement), but it is an alternative for programmers who just want to specify at a level that closer to code and model-check specifications.
- hwayne 2y ago
  Every time I see a new TLA+ replacement my first thought is "Oooh this will be good for the 99% of normal stuff people do with TLA+." Then I look through some of the specs I've written with clients and find the one absolutely insane thing I did in TLA+ that would be impossible in that replacement. Shoutout to operator labels.
  - setheron 2y ago
    So for us normies does that mean skip TLA?
    - hwayne 2y ago
      None of the replacements I've seen so far are mature enough for me to recommend them over TLA+.
      - igornotarobot 2y ago
        I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago was probably an exception to that. The other companies wish to immediately hide these tools and the benchmarks behind the IP and closed source. As a result, we have early stage MVPs that are developed by 1-3 people.
pnathan 2y ago
I don't see any peer reviews of quint's work on their site or GitHub. Am I missing them?
- igornotarobot 2y ago
  When you say peer reviews, do you mean academic publications or testimonials? I imagine it would be difficult to publish a paper at an academic conference proposing an alternative syntax for anything, even if it were better.
bvrmn 2y ago
It's kinda raw at this point of development. Could be a promising alternative for pluscal.

mjb 2y ago

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 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.

vosper 2y ago

bokumo 2y ago

What LaTeX package does one use to get the "back" link at the end of footnotes like the linked PDF exhibits?

gurjeet 2y ago
Yes, that's an interesting implementation. I'm using Firefox, and the jumps to the notes and back to the paragraph are recorded in history, and has the expected effect when clicking the back and forward history arrows/buttons.
evomassiny 2y ago
hyperref does this with the "\ref{}" command, it can link to any defined \label

leogss27 2y ago

[flagged]

Mathnerd314 2y ago

> Simplicity is a major goal of TLA+. 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.

colanderman 2y ago
TLA+ is only "executable" in the same sense that an algebraic expression is executable. It's perfectly possible to write things on TLA+ that can not be simply executed linearly. (These overlap to a great extent with the things which TLC rejects.) As a basic example, it's easy to write a statement with \A (unbounded universal quantification) whose truth can only be judged by a proof engine. Specification languages are explicitly not programming languages, for the core reason that programming languages dictate only what must occur; whereas specification languages can dictate what must not occur. It's not possible with a "specification" written using a programming language to determine what of a program is actually the specification, vs. what is an accident of the implementation.
- AlotOfReading 2y ago
  Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages. More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases. TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be, not because there's some universal line dividing specification languages from programming languages. It's also one of the biggest hurdles to TLA+ usage.

wizerno 2y ago

As someone who's fascinated by formal verification and who's early in their career, what advice do senior folks who have been using TLA+ have? 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!

kadoban 2y ago
There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.
- mnk47 2y ago
  >There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. I guess this must be true on places like SF since I see this so often on HN, but almost every single job listing I've seen strictly requires knowledge of a specific tech stack, with the exception of a few internship programs.
  - Turfie 2y ago
    Exactly my thoughts as well.
  - kadoban 2y ago
    There's tech that if it's not on your resume, you won't pass the first filter. But that's different. Knowing it will _not_ get you a job, it'll just get you past some early step. But things like TLA+ are way different from even that. The number of programming jobs that will bin you if you don't have TLA+ on your resume has to be like, 5 in the world. Nobody is going to see it on there and be like "we _must_ hire this person!".
SonOfLilit 2y ago

hwayne 2y ago

> The [\EE] operator is needed to explain the theory underlying how TLA+ is used. 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.

rtpg 2y ago

I'm really not a fan of TLA+'s tooling, but I do really love the temporal logic. I've always kinda wanted that stuff in other proving languages, but I don't know how possible it is. 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/Articles/An%20Axiomatization%20of%20Linear%20Temporal%20Logic%20in%20the%20Calculus%20of%20Inductive%20Constructions-Coupet-Grimal-2002.pdf https://lim.univ-reunion.fr/staff/fred/Enseignement/Verif-M2...

zozbot234 2y ago
> 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? Temporal logic is just a specific instance of a modal logic, which can be modeled with reasonable ease using a "possible worlds"-based encoding. Note that TLA+ combines temporal logic with non-determinism, which is a different modality.

pnathan 2y ago

I was looking at TLA a few months ago to consider what it would take to prove multiregion fail over worked correctly. Considering I'd never looked at it before. 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.

mjb 2y ago
I'd suggest starting with P (https://github.com/p-org/P https://github.com/p-org/P), or picking up Hillel Wayne's TLA+ book to get started.
- sriram_malhar 2y ago
  P is very nice indeed, be advised that it is not an exhaustive checker like TLC (TLA+'s model checker, or Apalache, the symbolic tester). It is more like a higher-level testing framework. That said, since non-deterministic choices are equi-probable in P, failure conditions are triggered at much higher frequencies than in a conventional testing scenario.
nektro 2y ago
https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html is really excellent

penguin_booze 2y ago

> The superscript 1 at the end of this sentence is a link to an end note; click on it now. 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.

jayaprabhakar 2y ago

TLA+ is 25 years old. Despite the power it's syntax is too alien to become mainstream. Have you considered https://FizzBee.io https://FizzBee.io? Almost Python-like syntax, has more powerful semantics, beautiful visualizations with no extra work, only formal methods system that can do performance analysis.