The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Interesting thread so far. I have few thoughts on performance, unsurprisingly. Just many thoughts on why I like dependent types (practically) and how much suffering is essential (much less than the status quo).

With dependent types, you can rule out entire classes of programs you don't want at compile-time, and get a nice specification for the user. So your user can know off the bat what weird edge cases your program disallows, and furthermore the user will not even be allowed to call the program with one of those edge cases. From that perspective, I expect that once we make these a bit easier to use, they will be a lot more common as a normal programming language feature.

Many of the pain points for using dependent types (especially the pain points for using indexed inductive types) are not at all fundamental and I am confident this will change in the near future. Indexed inductive types give some of the neatest specifications. And proof assistants are useful not just for proving things, but of course also for the inherent value that the specification that you've proven provides to the user.

There will always be some necessary suffering. When you have a dependent type, all of your programs are not just programs but also proofs of some invariant on the program. And all of your proofs about those programs also carry proofs about your invariant proofs, hence everyone's favorite axioms for dealing with equalities of equalities. But that should be the only necessary suffering.

If you look at really experienced programmers using dependent types, I find that often what they are doing (probably subconsciously) is constructing all of their dependently typed programs in such a way that the proofs relating those programs later on will go through trivially, for example by reflexivity. It would be fun to see if there is a way to partially automate this without relying on any axioms.

Talia

On Tue, Mar 3, 2020 at 11:44 AM Jason Gross <jasongross9 AT gmail.com> wrote:

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