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

 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.
 I too have a series of blog posts on TLA+ and verification in general aimed at working programmers. I'm giving a talk next month at a local developers' meet up on formal specifications and will probably cover TLA+ mostly (or maybe Dafny?).I'd love to read your posts. Is there a url or twitter account where I can get updates on your work?
 I expect to publish the posts starting in mid-May. My twitter handle is pressron
 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.
 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.)
 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, tooThis 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.
 I'm not sure what specific temporal properties you're interested in, but safety properties proven through the standard proof techniques (like inductive invariants), and at least common statements about liveness are supported.> Liveness is about infinite number of states, but any real model checking is bounded by definition.First, model checking is not bounded to a finite number of states in principle, and certainly not by definition[1]. Even in practice, modern, state-of-the-art model checkers do support infinite state spaces[2] -- of course, not in general, but in some cases. However, TLC, the model checker packaged with the TLA+ tools, is indeed not such a model checker, and can only check finite state spaces; it is what's known as an explicit state model checker. Second, liveness is not about an infinite number of states, but infinite behaviors, i.e. infinite sequences of states; the two are not the same.> but to prove liveness you are almost doomed to use temporal logic.Oh, absolutely, and after all, the TL in TLA stand for temporal logic, but the point is that proving complex liveness properties in real-world software systems is rare, simple liveness seems to be supported by TLAPS (although most people just use the model checkers), and complex temporal reasoning hardly ever comes up. That's why supporting complex temporal reasoning -- if it is indeed missing in TLAPS -- is not a priority. The features of TLA+ are in general very much driven by the needs of engineers working on real systems.However, if you happened to come across a liveness property you wanted to but couldn't prove with TLAPS, I'd love to hear about it.[1]: The name model checking comes from the model checking problem in logic, namely checking that a structure M (a program in the case of software) satisfies a logical proposition ๐, i.e., that M โจ ๐, or that M is a model of ๐. The name "model" comes from a logical model, i.e., a structure that satisfies a theory or a proposition.[2]: E.g., https://cpachecker.sosy-lab.org/
 > Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.I thought CSPm/FDR4 proved liveness on infinite event trails without temporal logic? Can't one extract "never" and "sooner or later" by just exploring the whole state space? Deadlock/livelock will never happen etc.
 Yes, but what if you are unable to explore the whole state space due to its unboundedness? Then the only way I know is by deducing properties thru temporal reasoning.

Search: