The Coq mailing list

[Xuanrui Qi <xuanrui AT nagoya-u.jp>]

> I would personally find it horrible if we omitted proofs from papers
> because a literate file exists

I'd agree in principle. Even if a literate formal proof exists, I feel
that we're obliged to at least state the high-level proof idea in
prose. Of course, there are always some complicated but uninspiring
proofs (e.g., many soundness proofs, proof by tedious but uninteresting
case analysis) which I feel OK to just omit.

Imagine if students go to their first, say, abstract algebra lecture
and find that they have to learn the proofs from a literate Coq file.
That would just be scary. Also, consider conferences like ITP and CPP;
one would still have to submit a regular-length paper accompanying
their formal proof. I think the answer is quite clear here --- formal
proofs, even literate proofs, are not a substitute for well-written
prose.

Xuanrui

On Sat, 2020-01-11 at 21:02 +0530, Siddharth Bhat wrote:
> I'm no expert at any of what's being discussed (lean, coq, math, or
> theoretical CS), but I feel that as an undergrad / hopeful grad
> student to be, it might be a useful perspective:
> 
> I personally find that even "literate" coq / agda code is quite often
> unreadable, coq more so that agda. The proofs tend to feel optimised
> for writing, not really for reading. Much of the Comp Cert proofs
> which I have read are tedious. The signal is honestly lost in the
> noise.
> 
> I would personally find it horrible if we omitted proofs from papers
> because a literate file exists --- papers are written to transmit
> understanding, formal proofs are mostly written to be verified (as
> far as I can tell) These are two different goals, and no current
> proof system in my experiences satisfies both goals.
> 
> Also,my two cents on smooth infitesimal analysis is that it is quite
> hard to build. We need to build algebras of polynomial rings over the
> reals to obtain models of infinitesimal analysis, which is non
> trivial. I don't know of a coq development of this. I'd like
> references if it does exist
> 
> Thanks,
> Siddharth
> 
> sent from my phone, please excuse any typos!
> 
> On Sat, 11 Jan, 2020, 14:47 Tadeusz Litak, 
> <tadeusz.litak AT gmail.com>
> wrote:
> > Hi Hugo,
> > 
> > On 11.01.20 05:22, Hugo Herbelin wrote:
> > >   I've known the Types community for
> > > now 30 years, a community who developed Agda, Coq, Isabelle,
> > Idris,
> > > Matita, Twelf, Alf, Lego, Epigram, ... a community who welcomed
> > NuPrl,
> > > Mizar, PX, the QED manifesto ... a community who will also now
> > invite
> > > Leo de Moura at its next conference in March in Torino. I'd be
> > happy
> > > to see this collaborative spirit being prolonged. There is indeed
> > so
> > > much to do in the building of proof assistants and interactive
> > theorem
> > > provers, towards better foundations, towards more expressive and
> > more
> > > intuitive proof languages, more robust and more expressive tactic
> > > programming languages and automation, more cooperative ecosystems
> > of
> > > libraries (and, probably, we should find here better ways to let
> > users
> > > and developers collaborate altogether).
> > 
> > Perhaps my comment about nobody being able to master simultaneously
> > all available proof assistants was likely to be 
> > misinterpreted. I never wanted to suggest that there should be just
> > one (or two or at most three) of them on the market.
> > 
> > It was in reaction to the specific claim that proofs on paper
> > became obsolete. I do not quite agree that it is enough to 
> > say "proofs are available as source code of such-and-such proof
> > assistant", especially in a mathematical paper. Software 
> > rot and the Tower of Babel problem are just two example reasons why
> > this is problematic.  The situation is made even 
> > worse by the way conference system works, encouraging people to
> > omit proofs from the body of the paper anyway.
> > 
> > Yes, it is obviously fine to omit trivial proofs, which would be
> > anyway dismissed as "exercises for the reader", "easy 
> > corollary", "trivial induction" etc.
> > 
> > It is also fine to use "literate" code in the paper, although what
> > is "literate" for a proficient user of one proof 
> > assistant might not necessarily be so for readers accustomed to
> > other systems and notations. And even the syntax of each 
> > specific proof assistant tends to change over time.
> > 
> > But the blunt statement that paper proofs "have outlived their
> > usefulness" and should be omitted altogether is not the 
> > right message to send, especially in the present state of affairs.
> > 
> > Best,
> > 
> > t.
> >