The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Tadeusz,

Your comment on nobody being able to master simultaneously all
available proof assistants is perfectly meaningful, and I personally
appreciated the quality of your different technical posts which are
totally relevant to the discussion.

Regarding Conor, as several persons actually privately expressed at
various degrees their perplexity on the point of his posts, it may be
good that he explains himself the actual message he's trying to
communicate. In any case, my feeling is that this is certainly not
against your own particular message but rather about more general
considerations.

Best regards and thanks for your contributions to the discussion,

Hugo

On Sat, Jan 11, 2020 at 10:16:18AM +0100, Tadeusz Litak 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).
> 

> 
> 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.