4 ms·

Could anyone with first-hand experience of TLA+ comment on how practical it actually is? I've been toying with idea of trying this for a not-quite-trivial (pro

Could anyone with first-hand experience of TLA+ comment on how practical it actually is? I've been toying with idea of trying this for a not-quite-trivial (programming!) project I'm working on, but the documentation and UX have so far kept me quite skeptical of using this "for real". The fact that I also can't turn the proof into a program in a semi-automated fashion also seems to indicate that there's at least some barrier where the "doubled" amount of work would be justified. (I'm more inclined towards something like Idris or LiquidHaskell which seem to support practical programming better and will probably let you get arbitrarily close to "proof" in any practical sense where proof will matter.) I take it that this was mostly about mathematics and not implementations of programs, which may not quite have the same trade-offs. I still would like to hear from anyone with direct experience :).

frankmcsherry 12y ago
I was formerly in the same lab as Leslie. As a side project, we (Tom Rodeheffer, mainly) used TLA to verify the correctness of Naiad's coordination protocol. The protocol is very simple (distributed reference counting), and my initial "proof sketch" was about two paragraphs long (and very unconvincing, apparently :). Tom's TLA+ version was closing in on 200 pages, available at http://research.microsoft.com/pubs/183826/paper.pdf http://research.microsoft.com/pubs/183826/paper.pdf A short publication about it, with some reflective discussion of why it was hard to write down, is at http://research.microsoft.com/pubs/199767/clock-verif2.pdf http://research.microsoft.com/pubs/199767/clock-verif2.pdf My understanding is that part of the problem was that Tom needed to explain (re-prove) many meta-facts we take for granted.
- toolslive 12y ago
  for distributed protocols, you might want to try Alloy. Basically it allows you to find counter examples (which are in this case scenarios). http://www2.research.att.com/~pamela/zave_podc.pdf http://www2.research.att.com/~pamela/zave_podc.pdf is a well known example, working on the Chord join/leave protocol.
- lomnakkus 12y ago
  Very interesting, thanks (and to the other sibling poster). > Tom's TLA+ version was closing in on 200 pages, available at [snip] This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking by computer-based proof assistants, but I digress... One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.) Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized? EDIT: Russel & Whitehead
  - SEMW 12y ago
    > I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized? http://us.metamath.org/mpegif/pm54.43.html http://us.metamath.org/mpegif/pm54.43.html (though using a slightly different set of axioms to R&W: http://us.metamath.org/mpegif/mmset.html#axioms http://us.metamath.org/mpegif/mmset.html#axioms)
- gone35 12y ago
  Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to already-established proofs from some common repository? Maybe future versions of TLAPS would benefit from such a thing? (Sorry if this already exists; I'm just an interested layman.)
  - qznc 12y ago
    For the Isabelle theorem prover I know the Archive of Formal Proofs [0]. [0] http://afp.sourceforge.net/ http://afp.sourceforge.net/
    - gone35 12y ago
      Damn; this is amazing stuff... I had no idea: (from [1]) so just get a local copy, set the path, and voila you can import... Wonderful. Thank you for sharing this! http://afp.sourceforge.net/using.shtml http://afp.sourceforge.net/using.shtml
ahelwer 12y ago
I've used it a bit for stuff inside Azure. It's difficult to find a problem where the model checker shines; state machines are far too simple (better to use P[1] or something similar), and something like cache coherence (the Hello World of real-world TLA+) isn't a problem I hit often. TLA+ isn't only a model checker & theorem prover, though. The language itself is an excellent high-level way of expressing system design. Recently I've been applying it to eventually consistent systems, and writing an idea in TLA+ is a great way to flesh out the concept and spot hidden assumptions or edge cases. Lamport knows this; in the introduction to his TLA+ book, he quotes: "Writing is nature's way of letting you know how sloppy your thinking is." Followed by his own expansion on the concept: "Our basic tool for writing specifications is mathematics. Mathematics is nature's way of letting you know how sloppy your writing is. ... The mathematics we use is more formal than the math you've grown up with. Formal mathematics is nature's way of letting you know how sloppy your mathematics is. The mathematics written by most mathematicians and scientists is not really precise. It's precise in the small, but imprecise in the large. Each equation is a precise assertion, but you have to read the accompanying words to understand how the equations relate to one another and exactly what the theorems mean. Logicians have developed ways of eliminating those words and making the mathematics completely formal and, hence, completely precise." Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in. You may also be interested in the AWS paper, which had excellent results.[2] [1] https://plang.codeplex.com https://plang.codeplex.com [2] http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am...
- lomnakkus 12y ago
  > Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in. This sounds very intriguing. It guess there's at least some learning curve, but maybe it'll be a fun experiment vs. P&P in future. ;)
mjb 12y ago
We use it at Amazon Web Services (http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am...) and have found it very practically useful.
- lomnakkus 12y ago
  Yes, thank you, that was very interesting and insightful -- I've read it before, in fact it sparked my initial interest in TLA+. Unfortunately this is not necessarily applicable for a "working programmer" aka "poor man without huge resources at his disposal". Maybe I should work on the latter problem and then start to apply TLA+. Or maybe it should be the other way 'round. :)

frankmcsherry 12y ago

I was formerly in the same lab as Leslie. As a side project, we (Tom Rodeheffer, mainly) used TLA to verify the correctness of Naiad's coordination protocol. The protocol is very simple (distributed reference counting), and my initial "proof sketch" was about two paragraphs long (and very unconvincing, apparently :). Tom's TLA+ version was closing in on 200 pages, available at http://research.microsoft.com/pubs/183826/paper.pdf http://research.microsoft.com/pubs/183826/paper.pdf A short publication about it, with some reflective discussion of why it was hard to write down, is at http://research.microsoft.com/pubs/199767/clock-verif2.pdf http://research.microsoft.com/pubs/199767/clock-verif2.pdf My understanding is that part of the problem was that Tom needed to explain (re-prove) many meta-facts we take for granted.

toolslive 12y ago
for distributed protocols, you might want to try Alloy. Basically it allows you to find counter examples (which are in this case scenarios). http://www2.research.att.com/~pamela/zave_podc.pdf http://www2.research.att.com/~pamela/zave_podc.pdf is a well known example, working on the Chord join/leave protocol.
lomnakkus 12y ago
Very interesting, thanks (and to the other sibling poster). > Tom's TLA+ version was closing in on 200 pages, available at [snip] This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking by computer-based proof assistants, but I digress... One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.) Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized? EDIT: Russel & Whitehead
- SEMW 12y ago
  > I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized? http://us.metamath.org/mpegif/pm54.43.html http://us.metamath.org/mpegif/pm54.43.html (though using a slightly different set of axioms to R&W: http://us.metamath.org/mpegif/mmset.html#axioms http://us.metamath.org/mpegif/mmset.html#axioms)
gone35 12y ago
Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to already-established proofs from some common repository? Maybe future versions of TLAPS would benefit from such a thing? (Sorry if this already exists; I'm just an interested layman.)
- qznc 12y ago
  For the Isabelle theorem prover I know the Archive of Formal Proofs [0]. [0] http://afp.sourceforge.net/ http://afp.sourceforge.net/
  - gone35 12y ago
    Damn; this is amazing stuff... I had no idea: (from [1]) so just get a local copy, set the path, and voila you can import... Wonderful. Thank you for sharing this! http://afp.sourceforge.net/using.shtml http://afp.sourceforge.net/using.shtml

ahelwer 12y ago

I've used it a bit for stuff inside Azure. It's difficult to find a problem where the model checker shines; state machines are far too simple (better to use P[1] or something similar), and something like cache coherence (the Hello World of real-world TLA+) isn't a problem I hit often. TLA+ isn't only a model checker & theorem prover, though. The language itself is an excellent high-level way of expressing system design. Recently I've been applying it to eventually consistent systems, and writing an idea in TLA+ is a great way to flesh out the concept and spot hidden assumptions or edge cases. Lamport knows this; in the introduction to his TLA+ book, he quotes: "Writing is nature's way of letting you know how sloppy your thinking is." Followed by his own expansion on the concept: "Our basic tool for writing specifications is mathematics. Mathematics is nature's way of letting you know how sloppy your writing is. ... The mathematics we use is more formal than the math you've grown up with. Formal mathematics is nature's way of letting you know how sloppy your mathematics is. The mathematics written by most mathematicians and scientists is not really precise. It's precise in the small, but imprecise in the large. Each equation is a precise assertion, but you have to read the accompanying words to understand how the equations relate to one another and exactly what the theorems mean. Logicians have developed ways of eliminating those words and making the mathematics completely formal and, hence, completely precise." Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in. You may also be interested in the AWS paper, which had excellent results.[2] [1] https://plang.codeplex.com https://plang.codeplex.com [2] http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am...

lomnakkus 12y ago
> Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in. This sounds very intriguing. It guess there's at least some learning curve, but maybe it'll be a fun experiment vs. P&P in future. ;)

mjb 12y ago

We use it at Amazon Web Services (http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am...) and have found it very practically useful.

lomnakkus 12y ago
Yes, thank you, that was very interesting and insightful -- I've read it before, in fact it sparked my initial interest in TLA+. Unfortunately this is not necessarily applicable for a "working programmer" aka "poor man without huge resources at his disposal". Maybe I should work on the latter problem and then start to apply TLA+. Or maybe it should be the other way 'round. :)