Hacker News new | ask | show | jobs
by alisonkisk 2042 days ago
> 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.
2 comments
GregarianChild 2042 days ago
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...

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