<div dir="ltr">(I somehow only replied to coq-club)<br><div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">---------- Forwarded message ---------<br>From: <b class="gmail_sendername" dir="auto">Jesper Cockx</b> <span dir="auto"><<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>></span><br>Date: Tue, Mar 3, 2020 at 10:37 PM<br>Subject: Re: [Coq-Club] Why dependent type theory?<br>To: coq-club Club <<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>><br></div><br><br><div dir="ltr"><div>Hi Jason,</div><div><br></div><div>There's many reasons for me to choose a dependently typed language:</div><div><br></div><div>- From a philosophical point of view, dependently typed languages are the only kind of language that have been given a meaning explanation (in the sense of Martin-Löf). This is important because it means I can grasp the meaning of each rule/axiom on a fundamental level, something that I never managed for set theory.</div><div>- From a practical point of view, in a dependently typed language I don't have to learn and use separate languages for writing programs and for writing proofs about them. In fact, by giving the write types to my programs I often do not need to give any proofs at all (i.e. correct-by-construction programming).</div><div>- Dependent type theory is constructive so I do not have to assume classical principles when I do not need them.</div><div>- Since expressions at the type level can compute in dependent type theory, there are many equalities that I do not need to reason about explicitly but just hold by definition/computation (although not as many as I would want).</div><div><br></div><div>As for other interactive theorem provers not based on dependent type theory, such as Isabelle or HOL4, I am mainly jealous of their excellent integration with automated theorem proving tools (e.g. sledgehammer) and their huge mathematical libraries. In a dependently typed languages, it is much harder to get everyone to agree on a definition because there are so many different ways to encode a concept. This has the effect that libraries are a lot more fragmented and everything is done in a more ad-hoc manner. <br></div><div><br></div><div>Another weak point of current implementations of dependent type theory is abstraction: you <i>can</i> make a definition abstract but that means it becomes an inert lump that stubbornly refuses to compute, so you lose most of the benefits of working with a dependently typed language. But I see these as reasons to continue to improve dependently typed languages rather than to abandon them.

</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 3, 2020 at 10:00 PM Viktor Kunčak <<a href="mailto:vkuncak@gmail.com" target="_blank">vkuncak@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div style="font-family:monospace,monospace;font-size:small">I would be also curious to hear answers to this questions!</div><div style="font-family:monospace,monospace;font-size:small">("Lots of people do it" seems like a very compelling answer.)</div><div style="font-family:monospace,monospace;font-size:small"><br></div><div style="font-family:monospace,monospace;font-size:small">Which bottlenecks are you referring to? Are they intrinsically tied to dependent types, or they are related to the treatment of propositions and equality in systems such as Coq?<br></div><div style="font-family:monospace,monospace;font-size:small"></div><div style="font-family:monospace,monospace;font-size:small"><br></div><div style="font-family:monospace,monospace;font-size:small">There are type systems overlayed on top of initially untyped languages (e.g. the language of Alloy Analyzer) and there are gradual types and designs like TypeScript for to initially untyped programming languages. ACL2 theorem prover for pure LISP, SPASS theorem prover for first-order logic, and "<cite><span>TLA+ model checking made symbolic</span></cite>" model checker for TLA+ all include techniques to recover types from an initially untyped language.</div><div style="font-family:monospace,monospace;font-size:small"><br></div><div style="font-family:monospace,monospace;font-size:small">Best regards,<br></div><div style="font-family:monospace,monospace;font-size:small"><br></div><div style="font-family:monospace,monospace;font-size:small">  Viktor<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 3, 2020 at 8:44 PM Jason Gross <<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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>
</blockquote></div></div>
</blockquote></div>
</div></div></div></div>