BTW, what is the justification for using dependent type rather than stating assumptions&#x2F;theorems directly in predicate logic over set theory (as in TLA+)?<p>Lamport has this to say on the matter:<p><i>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.</i><p><i>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.</i><p>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?