I'd love to read your posts. Is there a url or twitter account where I can get updates on your work?
THEOREM ASSUME NEW F, NEW G,
F โคณ G, F
PROVE โG
PROOF BY PTL
(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.)
> 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.
> 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/
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.
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.