The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

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.