The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

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.