The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I don't think we need to pick a side here (although most of you know where I stand!). I doubt there will be one hammer to nail all nails. And that's precisely one of the greatest thing Coq has: its support for a wide spectrum of proof processes. Remember that, at the moment, the Ssreflect plugin was developed to have finer control of the proof, with ideas that spread over vallina Coq. Similarly, there can be plugins to have better support for automation.

On Thu, Jan 24, 2019 at 9:34 AM Adam Chlipala <adamc AT csail.mit.edu> wrote:

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.