<div dir="ltr">I'm in the process of writing my thesis on proof assistant performance bottlenecks (with a focus on Coq), and there's a large class of performance bottlenecks that come from (mis)using the power of dependent types.  So in writing the introduction, I want to provide some justification for the design decision of using dependent types, rather than, say, set theory or classical logic (as in, e.g., Isabelle/HOL).  And the only reasons I can come up with are "it's fun" and "lots of people do it"<div><br></div><div>So I'm asking these mailing lists: why do we base proof assistants on dependent type theory?  What are the trade-offs involved?</div><div>I'm interested both in explanations and arguments given on list, as well as in references to papers that discuss these sorts of choices.</div><div><br></div><div>Thanks,</div><div>Jason</div></div>