<div dir="auto"><div>You might be interested in Lamport and Paulson's "Should Your Specification Language Be Typed?" (<a href="https://dl.acm.org/doi/10.1145/319301.319317" target="_blank" rel="noreferrer">https://dl.acm.org/doi/10.1145/319301.319317</a>). Lamport's publications page includes some commentary on how the paper came to be.<div dir="auto"><br></div><div dir="auto"><br></div>-Colin<br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 3, 2020, 14:44 Jason Gross <<a href="mailto:jasongross9@gmail.com" target="_blank" rel="noreferrer">jasongross9@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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>

<p></p>

-- <br>
You received this message because you are subscribed to the Google Groups "lean-user" group.<br>
To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:lean-user+unsubscribe@googlegroups.com" rel="noreferrer noreferrer" target="_blank">lean-user+unsubscribe@googlegroups.com</a>.<br>
To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/lean-user/CAKObCaqa5NZvJvU_ZpZek%2BOnVEOQETiYpisbgJXhPchMn6PLcQ%40mail.gmail.com?utm_medium=email&utm_source=footer" rel="noreferrer noreferrer" target="_blank">https://groups.google.com/d/msgid/lean-user/CAKObCaqa5NZvJvU_ZpZek%2BOnVEOQETiYpisbgJXhPchMn6PLcQ%40mail.gmail.com</a>.<br>
</blockquote></div></div></div>