5 ms·

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

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

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