The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Thanks for clarifying.  Probably the difference is in the level of 
automation, which, amped up sufficiently, tends to make proof scripts 
significantly slower but also more general.  My understanding is that 
Iris and CompCert choose the "faster but less general proof scripts" 
side of the trade-off.  It remains to be seen which style will work best 
for routine use by engineering teams in industry, and indeed it could 
turn out empirically that less automation (and thus less motivation for 
nested lemmas) wins!

On 1/24/19 2:48 AM, Ralf Jung wrote:
> Hi,
>
> just to give some more data, not *all* large-scale developments need nested
> lemmas.  Iris (including RustBelt and our other applications) doesn't, and 
> from
> what I was told, CompCert doesn't, either.
>
> This is not to diminish their importance for some landmark developments, but
> some of the discussion here made it sound like program verification was not
> possible in Coq without nested lemmas.  That is not the case.
>
> Kind regards,
> Ralf
>
> On 23.01.19 22:02, Adam Chlipala wrote:
> > Sorry for any offense given, Theo.  My only intention was to clarify that 
> > nested
> > lemmas are an essential feature for production-scale use of Coq ATM as far as 
> > I
> > can tell, so their implied deprecation by the Coq team, without a named
> > replacement with the same strengths, is scary.  (Earlier messages in this 
> > thread
> > may or may not deserve to be interpreted in that way.  I'm devoting limited
> > attention to watching coq-club, and I could easily misinterpret statements 
> > after
> > quick reading.) However, I'm interested which replacements the Coq team is
> > working on!  I only ask that the feature remain until the replacement(s) are
> > ready.  Coq really would be unusable without some feature of this kind, to 
> > work
> > on a lemma during proof of another, without forcing replaying of parts of the
> > original lemma's proof script each time a new lemma is added.
> >
> > On 1/23/19 3:38 PM, Maxime Dénès wrote:
> > > Adam, I understand your remark, but let's not forget that the "cool new
> > > stuff" we have in mind is often closely related to performance (which I
> > > know is dear to your heart).
> > Absolutely.  Amping up the baseline performance would help remove the need to
> > economize on rerunning proof scripts.  I'm just skeptical that the baseline
> > performance can be pushed high enough any time soon that it stops mattering 
> > that
> > scripts need to be rerun.  (You're probably also not claiming that holy grail 
> > is
> > attainable any time soon.)
> >
> > > For example, optimizations, delegation
> > > heuristics, caching and invalidation are easier to implement in a
> > > language where the structure of the document, the dependencies between
> > > objects and their scoping are simple. Nested lemmas are making such
> > > analyses more difficult. Which does not mean we should remove them, but
> > > we have to deal with complex trade-offs.
> > A caching mechanism for in-progress proofs could do the same job more 
> > elegantly,
> > with the right IDE support!  That is, if I can edit a lemma before the current
> > proof, but somehow the state of the current proof is saved well enough that I
> > can jump right back in later, then, AFAIK, that would satisfy everyone.  It
> > would look nicer in the work-in-progress .v file, too, and save time on
> > prettifying finished scripts.