The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

What comes first to my mind is my own experience 

that it is generally not possible to define nested recursive

functions such as eg MCarthy's F91

F91 x = if x > 100 then x - 10 else F91 (F91 (x+11))

w/o using dependent types because they allow you to express

properties of the output that you can feed into the type-checker

for termination.

On the other hand, proving properties after defining the function

does not work with nested calls because you need those properties

while constructing termination certificates.

Of course if you work in a framework where termination of all

functions is not required by the type-checker, then you won't

have such a constraint.

Same applies for proofs that require nested inductions.

Sometimes, it is also very convenient to pack terms with correctness

certificates. This happened on our automation of Diophantine

relations when formalization Hilbert tenth problem in Coq with

Yannick Forster.

Best,

Dominique

---

De: "Jason Gross" <jasongross9 AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>, "agda-list" <agda AT lists.chalmers.se>, coq+miscellaneous AT discoursemail.com, "lean-user" <lean-user AT googlegroups.com>
Envoyé: Mardi 3 Mars 2020 20:43:30
Objet: [Coq-Club] Why dependent type theory?

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"

So I'm asking these mailing lists: why do we base proof assistants on dependent type theory?  What are the trade-offs involved?

I'm interested both in explanations and arguments given on list, as well as in references to papers that discuss these sorts of choices.

Thanks,

Jason