4 ms·

> TLA+ is ... as powerful as Coq This is an astonishing claim. Can you formulate measure theory in TLA+?

• pron 10y ago
  1. Why would that be astonishing? The "+" in TLA+ is FOL + ZFC, the same foundation used for virtually all of math (except some branches of logic). 2. I am not a logician so I don't know of the formal particulars of measure theory, of any limitation ZFC has in formulating it, or of any TLA+ specific limitations in that regard. However, TLA+ is not a general proof assistant (it can certainly be used to prove general math theorems, it just wasn't designed for that task), but a language for specifying and reasoning about algorithms and large software systems. In that, it is as powerful as Coq. 3. There are completeness proofs for TLA, i.e., that anything that you can state about a computation, you can state in TLA, and anything you can prove about a computation you can prove in TLA. Now, this isn't quite accurate: TLA is a linear temporal logic, and there are some things that you can state and prove in a branching-time temporal logics that you can't in a linear logic, nevertheless, as Moshe Vardi says in Branching vs. Linear Time: Final Showdown[1], it makes more sense to prefer linear time logic because empirical evidence suggests that it's far more useful. There is one glaring downside: TLA is unable to reason about probabilistic algorithms[2]. However, it is possible to embed reasoning about computation in the + part of TLA (i.e. ZFC) and reason about probabilistic algorithms in that way, and I assume that this is how it would be done in Coq, too. So you could do everything in TLA+ without the TLA bit, but that would be inconvenient, as the natural representation of algorithms in TLA is especially convenient and the main justification for the approach. So I would be very interested in seeing an extension of TLA meant to deal with probabilistic algorithms. 4. In the end, what matters isn't theoretical strength (by which Coq and TLA+ are equivalent in anything that concerns algorithms), but convenience. I am sure that there are some problems that are easier to formulate and reason in Coq than in TLA+. But the fact that no one has ever used Coq for a large software system, and that the handful of use cases in industry were always done in cooperation with academic experts while TLA+ is used in very large projects by "plain" developers speaks volumes to the strength of the approach. [1]: https://www.cs.rice.edu/~vardi/papers/etaps01-ver13.pdf https://www.cs.rice.edu/~vardi/papers/etaps01-ver13.pdf [2]: You can describe any probabilistic algorithm in TLA (i.e., state that an algorithm performs a certain step with a certain profitability). What you can't do is then state a probabilistic theorem about that algorithm, as "in 70% of the cases, the algorithm gives the right answer".
  • tome 10y ago
    Because Coq was designed (as I understand it) to help people prove theorems about mathematics, not about algorithms. If TLA+ -- a language designed to prove theorems about algorithms, not about mathematics -- is actually better for that purpose then a lot of people have wasted a lot of time. Sure, algorithms are mathematical and much of mathematics can be recast as algorithmic, but still they have quite a different flavour. If a tool designed to help with one is actually the best tool to to help with the other, then that is astonishing.
    • pron 10y ago
      > is actually better for that purpose then a lot of people have wasted a lot of time. I don't think it's better, but it is as mathematically powerful, certainly when within the realms of ordinary math. As it is not designed for this task, I would assume that Coq would be more convenient. Coq is a full decade older than TLA+ (and Lamport mentions Coq when he discusses the design of TLA+ as something to avoid because of the arcane, virtually unknown math; even the TLA logic is 5 years younger than Coq), and even Coq isn't the first theorem prover, nor the most popular. It wasn't even designed to be the "best" math prover, but (I would imagine) to be a tool for type theorists to see how well how their ideas work. After all, Isabelle (which preceded Coq and serves as a TLAPS backend) is very good at "general" logic (not type theory). BTW, TLA+'s proof languages looks very different from Coq, and is declarative in nature. It is based on Lamport's "how to write a proof", and, as I understand, Isabelle's Isar is also inspired by that style[1], so TLAPS looks a lot more like Isar. Also, remember that the very concept of machine-checked formal proofs of mathematical theorems are currently used mostly by people who design those provers and hobbyists. Few mathematicians are keen on the approach (although I think they should be). Proof of software correctness, OTOH, is something that a larger group is interested in. But back to my main claim: TLA+ lets you express specifications about a program that are as rich as anything Coq would let you do. It was designed by people who are experts in software specification rather than by type-theorists. I would guess that Coq may be a better for some things (maybe proving general theorems about some classes of programs), but when it comes to actually reasoning about large software in the industry, TLA+ and its older kin (Z, B-method and more) are almost the only game in town. Isabelle is also ahead of Coq in verifying real-world systems. [1]: http://isabelle.in.tum.de/Isar/isar-thesis-Isabelle2002.pdf http://isabelle.in.tum.de/Isar/isar-thesis-Isabelle2002.pdf