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.