The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I'm probably an outlier on this topic.  The point of my project was to
use dependent types as a way to guide a less experienced user (perhaps
an experienced software enginner with little proof background) to a
proof. Although, I only had myself as model for "less experienced
user".  The goal was to enable such a user to generate proven-correct
code from program specifications, where the specifications included
comprehensive invariants which are coded as dependent types.

What dependent type encoded invarants do to a proof is that the
constraints they impose make much clearer what can and can't be
accomplished in each proof step, freeing the user from having to
conceptualize the overall proof, and limiting the amount of proof
exploration (trial and error) needed.  They also enable a back
translation from a proof dead end to some understanding
about why the developing algorithm won't work (i.e.: such-and-such
invariant is now impossible to maintain due to these particular
proof steps).  In this way, a proof assistant becomes a programming
assistant.

The generated code had all of the dependent type aspects erased, as
they were all in Prop.

I don't know how this can be accomplished without dependent types.
Especially given a user that may have a very good understanding of what
particular dependent types encode in terms of invariants, but has
little or no experience with proof techniques and probably no theory
background at all.

I don't think I ever hit any performance bottlenecks in this
development that weren't related to the various (e)auto proof search
automations doing a less than impressive job of pruning the search.  I
have an example that I proved both with and without (e)auto proof
search - without it takes coqtop less than 7 minutes to complete on my
rather dated hardware.  With (e)auto, it takes about 2 hours.

On Tue, 3 Mar 2020 14:43:30 -0500
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