5 ms·

I have a passing familiarity with proof assistants such as Cow and HOL. How would you compare TLA+ with those? https://en.m.wikipedia.org/wiki/Coq https://en.m

by gghh 10y ago

I have a passing familiarity with proof assistants such as Cow and HOL. How would you compare TLA+ with those? https://en.m.wikipedia.org/wiki/Coq https://en.m.wikipedia.org/wiki/Coq https://en.m.wikipedia.org/wiki/HOL_(proof_assistant) https://en.m.wikipedia.org/wiki/HOL_(proof_assistant)

ahelwer 10y ago
Great question! So, TLA+ does have a machine-checked proof system called TLAPS, but its intended use is quite a bit different than Coq. While Coq is very well-suited for doing deep reasoning about mathematics and proving all sorts of stuff about whatever mathematical construct you care to define, TLAPS is focused much more on "mile wide, inch deep" type proofs required to demonstrate correctness of algorithms. Most algorithms use very simple mathematical properties, but have a bunch of edge cases and cyclomatic complexity which TLAPS is well-equipped to handle. There might come a day where TLAPS is as powerful as Coq for writing general mathematical proofs (indeed, better ways of writing proofs and mathematics seem to be a passion of Dr. Lamport's, see his paper How to Write a 21st Century Proof[0]), but for now it's far, far easier to prove even simple statements about the Natural numbers in Coq. [0] http://lamport.azurewebsites.net/pubs/proof.pdf http://lamport.azurewebsites.net/pubs/proof.pdf
pron 10y ago
This is a complicated question. I am currently writing a blog post series on the theory of TLA+ that I will publish in May that, among other things, touches precisely on this point. But I will try to quickly point out some areas of difference, but the most important thing to remember is that both Coq and TLA+ -- as far as specifying and verifying software is concerned (not general math) -- are universal formalisms. Ultimately, anything you can do in TLA+ you can do in Coq and vice-versa. Also, when using mechanical proof to verify software, the proof techniques and the actual work is pretty much the same. 1. Difference in theory -- the theory of computation in Coq and HOL is based on functional programming; especially in Coq (I know very little about HOL), algorithms are functions in the FP sense (lambda expressions). In TLA, algorithms are state machines, and there's a richer notion of relationship between algorithms. This makes some things easier in TLA: Instead of programs being equal extensionally or definitionally, they can be equal or similar in many ways. In fact, in TLA there's a partial order relation on algorithms that reflects the refinement/abstraction relation. Also, it means that different kinds of algorithms -- sequential, concurrent, parallel, realtime etc., are all defined in the same way using the exact same ideas. This also makes it very easy to specify some properties -- such as worst-case complexity -- that are tricky in Coq. Having said that, people working on realtime systems in Coq implemented a simple version of TLA in Coq. 2. Differences in goals and audience -- Coq and HOL are ultimately general mathematical proof assistants. TLA+ is a tool for reasoning about digital systems. Coq and HOL can obviously reason about programs and TLA+ can prove general math theorems, but the focus is different. For example, Coq is used by logicians to explore new logics and mathematical foundations; you don't want to use TLA+ for that. On the other hand, TLA+ is used by "ordinary" engineers in industry working on "ordinary" software, while Coq and HOL are virtually unused in industry, and in the few cases they are, it's almost always in conjunction with academics and academic projects. 3. Differences in tools/abilities -- Coq can generate runnable code and be used for end-to-end verification. TLA+ cannot generate code, and while it has been used by academics for end-to-end verification, that is most certainly not its intended use. It is intended to be used in modeling large, complex systems at an abstraction level that's significantly higher than the code to find errors in design. As far as general math proofs are concerned, Coq is more capable than TLAPS, the TLA+ proof system. On the other hand, TLA+ has a model-checker that makes its proof checker almost irrelevant for large, complex specifications. As the users of TLA+ usually don't require a 100% watertight end-to-end specification, they're content to get the less than 100% guarantee of the model checker in exchange for what is at least a one order of magnitude reduction in effort. In short, I would say that tools like Coq have a more academic focus, and are in general more interesting to academics and less to engineers, while TLA+ has a more industrial focus, and is of more interest to engineers and less to academics. But I will repeat and say that while there are big difference in theory, goals and usage, ultimately when working on verifying software, the challenge is in thinking about your system mathematically and understanding how and why it works (or not). This work is similar both in effort and technique no matter what formalism you choose to use.
- unboxed_type 10y ago
  AFAIK, TLAPS does not support temporal reasoning in full currently, so you are not able to prove liveness properties of your system. On the other hand, Coq is able to express both LTL logic and infinite trace, so you can prove such things in it.
  - pron 10y ago
    TLAPS supports temporal reasoning. I've personally used it only for safety (inductive invariant), but to make sure it supports liveness, I just checked the following: THEOREM ASSUME NEW F, NEW G, F ⤳ G, F PROVE ◇G PROOF BY PTL and it works fine (PTL stands for propositional temporal logic). I suppose there are some things that aren't supported (TLAPS has quite a few missing features), but TLAPS is very new by proof-system standards. Note that in general, TLA+ tries to avoid temporal logic as much as possible. Lamport has repeatedly said "temporal logic is evil". A 1000-line spec, will probably have no more than a couple of uses of temporal operators. (Of course, most people don't bother writing proofs at all for real, large, complex software as that is just too costly. They just use the model checker, that can check liveness, too.)
    - unboxed_type 10y ago
      Temporal reasoning is a lot more than that you mentioned, so by providing this example you can not conclude that TLAPS support temporal reasoning. I have read several papers of S.Merz, Lamport's student and now a researcher, who mentioned that there is no temporal reasoning apparatus available in TLAPS. Maybe something have changed since then but I found no evidence for this. > They just use the model checker, that can check > liveness, too This is not quite true. Liveness is about infinite number of states, but any real model checking is bounded by definition. For an engineer this is not a problem at all, but as for comp.sci researcher your ability to use TLA+ is limited in this respect. > Lamport has repeatedly said "temporal logic is evil" Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.
      - 10y ago

by gghh 10y ago

ahelwer 10y ago

Great question! So, TLA+ does have a machine-checked proof system called TLAPS, but its intended use is quite a bit different than Coq. While Coq is very well-suited for doing deep reasoning about mathematics and proving all sorts of stuff about whatever mathematical construct you care to define, TLAPS is focused much more on "mile wide, inch deep" type proofs required to demonstrate correctness of algorithms. Most algorithms use very simple mathematical properties, but have a bunch of edge cases and cyclomatic complexity which TLAPS is well-equipped to handle. There might come a day where TLAPS is as powerful as Coq for writing general mathematical proofs (indeed, better ways of writing proofs and mathematics seem to be a passion of Dr. Lamport's, see his paper How to Write a 21st Century Proof[0]), but for now it's far, far easier to prove even simple statements about the Natural numbers in Coq. [0] http://lamport.azurewebsites.net/pubs/proof.pdf http://lamport.azurewebsites.net/pubs/proof.pdf

pron 10y ago

This is a complicated question. I am currently writing a blog post series on the theory of TLA+ that I will publish in May that, among other things, touches precisely on this point. But I will try to quickly point out some areas of difference, but the most important thing to remember is that both Coq and TLA+ -- as far as specifying and verifying software is concerned (not general math) -- are universal formalisms. Ultimately, anything you can do in TLA+ you can do in Coq and vice-versa. Also, when using mechanical proof to verify software, the proof techniques and the actual work is pretty much the same. 1. Difference in theory -- the theory of computation in Coq and HOL is based on functional programming; especially in Coq (I know very little about HOL), algorithms are functions in the FP sense (lambda expressions). In TLA, algorithms are state machines, and there's a richer notion of relationship between algorithms. This makes some things easier in TLA: Instead of programs being equal extensionally or definitionally, they can be equal or similar in many ways. In fact, in TLA there's a partial order relation on algorithms that reflects the refinement/abstraction relation. Also, it means that different kinds of algorithms -- sequential, concurrent, parallel, realtime etc., are all defined in the same way using the exact same ideas. This also makes it very easy to specify some properties -- such as worst-case complexity -- that are tricky in Coq. Having said that, people working on realtime systems in Coq implemented a simple version of TLA in Coq. 2. Differences in goals and audience -- Coq and HOL are ultimately general mathematical proof assistants. TLA+ is a tool for reasoning about digital systems. Coq and HOL can obviously reason about programs and TLA+ can prove general math theorems, but the focus is different. For example, Coq is used by logicians to explore new logics and mathematical foundations; you don't want to use TLA+ for that. On the other hand, TLA+ is used by "ordinary" engineers in industry working on "ordinary" software, while Coq and HOL are virtually unused in industry, and in the few cases they are, it's almost always in conjunction with academics and academic projects. 3. Differences in tools/abilities -- Coq can generate runnable code and be used for end-to-end verification. TLA+ cannot generate code, and while it has been used by academics for end-to-end verification, that is most certainly not its intended use. It is intended to be used in modeling large, complex systems at an abstraction level that's significantly higher than the code to find errors in design. As far as general math proofs are concerned, Coq is more capable than TLAPS, the TLA+ proof system. On the other hand, TLA+ has a model-checker that makes its proof checker almost irrelevant for large, complex specifications. As the users of TLA+ usually don't require a 100% watertight end-to-end specification, they're content to get the less than 100% guarantee of the model checker in exchange for what is at least a one order of magnitude reduction in effort. In short, I would say that tools like Coq have a more academic focus, and are in general more interesting to academics and less to engineers, while TLA+ has a more industrial focus, and is of more interest to engineers and less to academics. But I will repeat and say that while there are big difference in theory, goals and usage, ultimately when working on verifying software, the challenge is in thinking about your system mathematically and understanding how and why it works (or not). This work is similar both in effort and technique no matter what formalism you choose to use.

unboxed_type 10y ago
AFAIK, TLAPS does not support temporal reasoning in full currently, so you are not able to prove liveness properties of your system. On the other hand, Coq is able to express both LTL logic and infinite trace, so you can prove such things in it.
- pron 10y ago
  TLAPS supports temporal reasoning. I've personally used it only for safety (inductive invariant), but to make sure it supports liveness, I just checked the following: THEOREM ASSUME NEW F, NEW G, F ⤳ G, F PROVE ◇G PROOF BY PTL and it works fine (PTL stands for propositional temporal logic). I suppose there are some things that aren't supported (TLAPS has quite a few missing features), but TLAPS is very new by proof-system standards. Note that in general, TLA+ tries to avoid temporal logic as much as possible. Lamport has repeatedly said "temporal logic is evil". A 1000-line spec, will probably have no more than a couple of uses of temporal operators. (Of course, most people don't bother writing proofs at all for real, large, complex software as that is just too costly. They just use the model checker, that can check liveness, too.)
  - unboxed_type 10y ago
    Temporal reasoning is a lot more than that you mentioned, so by providing this example you can not conclude that TLAPS support temporal reasoning. I have read several papers of S.Merz, Lamport's student and now a researcher, who mentioned that there is no temporal reasoning apparatus available in TLAPS. Maybe something have changed since then but I found no evidence for this. > They just use the model checker, that can check > liveness, too This is not quite true. Liveness is about infinite number of states, but any real model checking is bounded by definition. For an engineer this is not a problem at all, but as for comp.sci researcher your ability to use TLA+ is limited in this respect. > Lamport has repeatedly said "temporal logic is evil" Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.
    - 10y ago