I never said that Coq is an academic toy. Some projects done in academia and used in the industry have been verified with Coq, but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any).

> I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is

I've never said it is unreasonable, only that it is foreign to most engineers (as well as most academic CS people), or rather, more foreign than basic logic/set theory.

I would say again that if you're comfortable with type theory, you might enjoy Coq better. If not, TLA+ would probably be more approachable. TLA+ has the added advantage of having a model checker, which is very useful when you don't have the resources required for a full proof, but still want a good confidence in the correctness of your algorithm.

> A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement!

Oh, absolutely! It's just that stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most. TLA+ is a good entry point to formal methods, even if you later choose to move to dependent-type approaches and tools.

The first EAL7 certified smart card certification used coq, see: https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pd...

They mention > 117,000 lines of Coq with > 1600 proofs to get EAL7 for the JVM.

Lamport has this to say on the matter:

The main virtue of these type theories is precisely that they are constructive. A constructive proof that two arbitrary numbers always have a greatest common divisor provides an algorithm for computing it [Thompson 1991]. Researchers, using tools such as Coq and Nuprl are investigating whether this can lead to a practical method of synthesizing programs.

You can perform classical reasoning in a constructive type theory by adding P ∨ ¬P as an axiom. The resulting system will probably be strong enough to handle any specification problem likely to arise. However, it will be no stronger than ZF, and it will be much more cumbersome to use.

In the end, he opted for set theory because it is simpler, more familiar, and more flexible. Are there any advantages to using dependent types? Is the main advantage indeed synthesizing programs from proofs?

It's one major advantage, yes. And not just for the sake of software verification. Sometimes when proving a non-CS-type-math theorem you still want an efficient implementation of an existence proof.

But code synthesis is a lot harder than merely being constructive, and efficient code synthesis even more so. Use cases for Coq that depend upon code synthesis don't come for free just by avoiding LEM. So although it's fair to say that you can do classical reasoning in Coq, I'm not sure saying you can do synthesis from TLA+ if only you avoid LEM is fair at the moment (I might be wrong).

> Are there any advantages to using dependent types?

Here are a few other reasons for using Coq:

* Proof terms. There are two major disagreements here. The first grounds out in philosophy and the second basically amounts to "you really want to compose the proofs and make sure they are still a proof instead of just throwing away the proof and using the theorem" which has lots of good systems-y justifications

* Specifically wrt TLA+, Modus Operandi matters. If you want a formal proof in the typical sense of the word (rather than a verification of fact based upon model checker output), then Coq userlands's tactics and theorems are useful.

* Lots of people like to disparage the amount of algebra that FPers talk about. But it turns out that if studying those algebraic structures is your day job, the relationships between types and algebraic structures makes type theory convienant.

>simpler, more familiar

This is almost definitionally subjective. Which isn't meant as a criticism, in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar.

> and more flexible

There are (obviously) a lot of people who fundamentally disagree with the concrete arguments Lamport makes in this paper. I wish someone would annotate the paper with references to literature from the type theory community that address some of his concerns.

For the record, I don't disagree with Lamport. I think Lamport is right -- for some use cases, it certainly makes sense to stick with ZF. But he's also wrong -- sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation.

TLA+ has them, too.

> in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar.

So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)?

> sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation

I don't see it (probably because my type theory is very, very basic; I'm an algorithm's guy and the thought that a data-structure of mine might need type theory to be specified makes me shudder), as in I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain?

Like I said, modus operandi matters. If I have to perform another model checking routine (possibly on an infinite state space) to slightly generalize a theorem, then in many cases that means I never really had a useful proof of it in the first place.

Also, Coq's mathematics library is extensive and often closely follows the proofs found in graduate mathematics text books. Last I looked into TLA+, it was squarely focused on algorithms and hardware (not even CS-related mathematics more generally -- specifically algorithms and hardware).

> So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)?

Do I think there exists some population of people who are "more familiar" with type theory than with ZF? Yes, starting, for example, with every researcher whose primary area of study is type theory. In fact, I think that anyone who doesn't honestly believe there are such people must have an extremely low opinion of quite a number of very smart people.

(Also, set theory qua set theory gets really disgusting and kludgey really quickly, and is something that almost no undergraduate (or even phd student) is exposed to these days. The "set theory" you see in a discrete math course kind of barely scrapes definitions. I think most people who posit that "set theory" is nice and simple must've never really dove deem into the actual theory of set theory...)

(Also, most real math these days quickly abstracts away from germanely set theoretic constructions. Mathematicians don't work in ZF. They do not. Most will tell you they do not, if they even know what ZF is. Which a lot won't, because their undergrad discrete math course is probably the last time they saw a truly formal derivation. And the mathematicians who do know what ZF is often can't regurgitate an axiomatization of ZF. If you tell a mathematician that all of math is just set theory, most will chuckle and wink and say "why, yes, yes it is", and hopefully you're in on the joke...)

> I don't see it... I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain?

Did you read this dissertation's explanation of why separation logic is important?

To the extent that this observation is remotely reasonable, it's only in the sense that you can code up one logic in another. Which, well, all the world's a TM, as they say...

Anyways, I think the argument over whether type theory is a successful foundations for CS research and practice is already a closed issue. It demonstrably is. So is set theory.

Why model checking? TLA+ is not a model checker. It's a specification and proof language. There is a model checker that can check TLA+ specs, just as there is a proof assistant that can check TLA+ proofs.

> must have an extremely low opinion of quite a number of very smart people.

Why low opinion? Type theory isn't "smarter", it's just more obscure.

> The "set theory" you see in a discrete math course kind of barely scrapes definitions. I think most people who posit that "set theory" is nice and simple must've never really dove deem into the actual theory of set theory...

Thankfully, that basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs.

> Did you read this dissertation's explanation of why separation logic is important?

Skimmed it. Unless I'm missing something (which is quite possible) it seems very straightforward to use in TLA+: you just define the operators just as they're defined in the paper. There's no need to "code" the logic in any arcane or non-obvious way; just define it. In fact, this short paper describes doing just that and it seems pretty basic: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.570...

> Anyways, I think the argument over whether type theory is a successful foundations for CS research and practice is already a closed issue. It demonstrably is.

It never even crossed my mind to make the case that it isn't. That type theory is an interesting topic for research is obvious. I also never implied that dependent-type tools can't do the job; as you say, they demonstrably can. I simply asked if I -- a programmer working in the industry -- had a program I wished to verify, whether there was a reason why I would reach for a dependent-type tool vs. a classical logic tool. So far, I don't see why I should. It seems to basically boil down (at least according to the responses in this thread) to whether I prefer working with direct, classical logic or with dependent types.

For the third (!) time, modus operandi matters.

Coq's huge library of tactics and proofs of facts that TLA+ might just throw at a model checker are, in my experience, very useful starting points for things that can't be model checked.

Ostentibly TLA+ could build up an equivalent library of tactics and proofs.

> Why low opinion?

Even supposing type theory is "more obscure", it's pretty hard to believe that someone could study it for 30 years and not understand it better (in some sense) than ZF. That's a pretty extraordinary claim.

> basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs.

Not really -- you often need non-trivial constructions when proving properties about rewrite systems within set theory. Those constructions are much harder to understand than induction on algebraic datatypes, which is why type theoretic approaches have dominated in formalization of programming languages.

>Unless I'm missing something...

I'm disinclined the dismiss separation logic just because you can code up some of its ideas in another logic (in a way that counts as a novel contribution worthy of publication, no less).

The clarity with which separation logic presents the idea and use of the separating conjunction has obviously influenced the paper you cited. I would think this is reason enough to summarily dismiss these "everything's a TM"-style arguments you're making here. The authors of the paper you cited are only not using separation logic in a kind of meaningless sense IMO.

> So far, I don't see why I should.

This sentiment kind of reminds me of people who have never typeset mathematics complaining that LaTeX is useless... which is to say, perhaps you simply aren't interested in and so don't care about the use cases where Coq shines? Lots of people -- including me -- have already pointed out a lot of these use-cases in this comment section.

But really, based on the arc of this conversation, I would be enormously surprised if you chose to use Coq to prove X, even if there were a proveX tactic already written in Coq and the TLA+ implementation would take all day ;-)

I don't understand what you're saying. What does TLA+ have to do with the model checker? TLA+ is a language, while TLAPS (the proof system) and TLC (a model checker) are two different products (each supporting different subsets of TLA+, BTW). TLAPS comes with its own library of proofs. I don't know how extensive they are.

AFAIK, you can't (and certainly you don't) take a fact verified by the model checker and state it as an axiom of your proof. The interaction between the two -- if any -- is that Lamport encourages you to model check your spec before trying to prove it (assuming you want to prove it, or even model-check it) because proving things that are false may prove hard. However, the result of the model checker play no part in the proof.

When it comes to proofs, TLA+ is intended to be declarative and independent of the proof engines used (by default, TLAPS uses SMT (any of several solvers), Isabelle and another couple of tool, passing every proof step to every tool unless a tactic specifies a particular one).

This is a nice introduction for the design of the TLA+ proof language: http://research.microsoft.com/en-us/um/people/lamport/pubs/p... which includes (in the appendix) a few proofs in calculus.

> it's pretty hard to believe that someone could study it for 30 years and not understand it better (in some sense) than ZF. That's a pretty extraordinary claim.

I did not mean to claim that type theory researchers don't understand it better than basic college set-theory. I meant that in general, engineers and academics are more familiar with basic set theory.

> just because you can code up some of its ideas in another logic (in a way that counts as a novel contribution worthy of publication, no less).

That was a technical report that mentioned in passing using an approach similar to separation logic.

> "everything's a TM"-style arguments you're making here

I am not making that argument. My argument is that most engineers and CS academics (except those in PLT) would be more familiar -- and therefore more likely to use -- a tool based on basic math they know well. In addition, I haven't seen anything to suggest that the complexity difference between specifying a system using dependent types and specifying it in TLA+ is significant at all in either direction. Learning Coq, however, requires much more effort, and AFIK, it doesn't support formal verification mechanisms other than proofs (e.g. model checking)

> perhaps you simply aren't interested in and so don't care about the use cases where Coq shines?

Perhaps. I design data structures (mostly concurrent), and my interests lie in specifying and verifying those as well as distributed systems, and less in verifying compilers. My current TLA+ spec is too complex to be proven anyway (regardless of the tool used) in any feasible amount of time, so I rely on just the spec as well as some model checking.

It is also true that I may be biased. As an "algorithms guy" I feel more at home working with tools and languages designed by other algorithm people (and more importantly for algorithm people) rather than PLT people.

Nevertheless, I'm interested in learning the difference between the two.

> But really, based on the arc of this conversation, I would be enormously surprised if you chose to use Coq to prove X, even if there were a proveX tactic already written in Coq and the TLA+ implementation would take all day

Considering that learning Coq would take me much longer than a day, that would be a wise decision.

For instance, in higher-order set theory a (very strong) form of the axiom of choice asserts that there is a function "epsilon : set -> set", such that "epsilon x \in x" for x not empty. Expressing the same in first-order ZFC turns the whole statement on its head since you need to encode this function somehow. This leads to (almost) equivalent but misleading statements, such as "the intersection of a set all of whose inhabitants are non-empty is non-empty". Now if you look into TLA+, you will find that this choice operator epsilon has been added to the language, because it is so useful in practice! And this is just one instance of something that "type-theory" can add over classical ZFC. More to the point, higher-order specifications are crucial for the verification of higher-order programs. Higher-order programs are in turn one of the most useful tools for writing modular code.

Sorry for the nitpicking; let me get back on topic.

The main advantage of Martin-Löf style type theory is that it makes it easy to build new abstractions. For instance, the Bedrock project (http://plv.csail.mit.edu/bedrock/) builds an extensible program verification environment within Coq. This is only possible because the underlying logic is so expressive that you can build internal models for whichever pet logic you want to reason in. From a practical point of view dependent types and the conversion rule - computations in proofs - allows you to build scalable (reflective) proof automation while retaining a small trusted base.

The constructive aspect of Martin-Löf type theory is very pleasing from a philosophical point of view, but again in practice it's not the most relevant aspect. The main reason for me to use something other than classical logic is that there are more models of intuitionistic logic than of classical logic. This gives you more freedom in designing a logic which makes it easy to reason about your particular problem domain. For instance, if you work with Cyberphysical systems, you might like to work within the framework of synthetic differential geometry where all functions are smooth and the real numbers are as simple as they can ever be.

What so many people seem to be ignoring is that the logic you use for reasoning is part of your design space. Saying "I'll just use ZFC" is exactly the same as a programmer exclaiming "I'll just use COBOL". Leslie Lamport designed TLA+ to make it easy to reason about distributed systems. There may well be a nicer logic for reasoning about distributed systems, but you will probably not find it among the models of classical ZFC, since there aren't really that many of them...

On the other hand, there are many different flavors of type theory, just waiting to be discovered. And in my view that's the main advantage of looking beyond set theory.

Such higher-order statements are easily expressible in TLA+ as long as you specify the domain of the sets on which you operate, which you should always be able to do when specifying real programs, even higher-order programs. Here it is in TLA+:

     ∃ epsilon ∈ [SUBSET S → S] : ∀x ∈ SUBSET S : epsilon[x] ∈ x

> Saying "I'll just use ZFC" is exactly the same as a programmer exclaiming "I'll just use COBOL".

I don't think it's the same at all, considering that 99.9% of math is done with "just ZFC". I don't doubt that type theory may let us explore other logics, but as a practical way for specifying real programs today I fail to see a case in favor of dependent types. Sure, I believe dependent types may let you define all sorts of modal logic, but in practice, temporal logic has proven a good way to specify algorithms. So I think that a more suitable analogy would be, "Why confine your thinking to von-Neumann machines when you can use a meta-logic to specify programs for Quantum computers and other computational models". In that case, "I'll just use a von-Neumann machine" seems like a very reasonable choice for any work that isn't theoretical.

But this is missing the point. There is a lot of active research work on program logics for reasoning about e.g., concurrent programs in weak memory models. You may be able to encode the model of something like Iris (http://plv.mpi-sws.org/iris/) in TLA, but the challenge lies in doing this in a usable format...

All the constructions I know use at least second order logic and something like Iris is - as far as I know - most elegantly described internal to the topos of trees. If you have found a good way to avoid this complexity then that's a significant contribution.

At the moment we're not open-sourcing the spec (I'm an engineer, not an academic) but we might in the future. We've opted not to even try to prove the system's correctness, as that might take decades (it's far more complex than, say, seL4). Instead, we're just formally specifying it, and model-checking it with a finite model. The software in question, however, is itself open-source and is described here: http://blog.paralleluniverse.co/2012/08/20/distributed-b-tre...

> All the constructions I know use at least second order logic

Concurrent algorithms are specified with TLA+ (in the industry, I mean) quite frequently. Also, specifying the memory consistency properties does require second order logic, but as I've shown in another comment, TLA+ handles second-order logic gracefully and in a very straightforward matter (trivially, I would say). You simply write:

∃ ordering ∈ [operations → SequenceOf(Op)] : ConsistencyProperty(ordering[operations])

    ∃ epsilon ∈ [SUBSET S → S] : ∀x ∈ SUBSET S : x ≠ {} ⇒ epsilon[x] ∈ x

    ∃ epsilon : ∀x : x ≠ {} ⇒ epsilon[x] ∈ x