Program extraction. In dependent type theory if you've proved "A implies B" you can extract from that proof a program that takes an argument of type A and alwa

Program extraction. In dependent type theory if you've proved "A implies B" you can extract from that proof a program that takes an argument of type A and always halts, returning a value of type B. Moreover if you prove some property about proofs that A implies B, you've also proved the corresponding proposition about programs. This means your proofs get to deal with programs directly, rather than having to formalize them as something like Turing machines whose tapes are set-theoretic encodings of lists of integers. It's excruciatingly painful to write non-hand-wavy proofs of anything that way. Hand-wavy proofs that can't be machine-checked aren't so bad of course; complexity theory folks have been doing that for decades. If you aren't proving things about programs or homotopy then there really aren't any obvious reasons to prefer dependent type theory. I say this as somebody who loves programming with dependent types. But I'm being honest here, and I wish more people in the mechanized mathematics world would be honest about this.