[octoberfranklin]

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.

[alisonkisk]

> there really aren't any obvious reasons to prefer dependent type theory

The OP gives a reason, and it's the same reason programs use types. Untyped proofs are usually wrong, like untyped programs.

[GregarianChild]

HOL is typed, but not a dependent type theory. HOL is also a classical logic. HOL is essentially Alonzo Church's simply typed lambda-calculus [1] from 1940. Classical, rather than constructive logic tends to give shorter proofs.

[1] A. Church, A Formulation of the Simple Theory of Types. https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b...

[octoberfranklin]

Er, no. Even Coq proofs are written in an untyped language (Ltac). You've got your levels mixed up.