> 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.

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.