The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Ah, poly.

Sent from my i

On 10 Jan 2020, at 20:30, Tadeusz Litak <tadeusz.litak AT gmail.com> wrote:



On 10.01.20 20:41, Timothy Carstens [or Adam Chlipala] wrote:

The reason is that the author and many other researchers today feel that proofs on paper have outlived their usefulness.

While I am fully supportive of proof assistants conquering both math and CS worlds, the present state of affairs does not seem to justify such a bold statement. I presume it was intended to be sell talk and supposed to be taken with a grain of salt, but even then it can be dangerously misleading. 

It might be applicable to a not-so-novel CS conference contribution, where the underlying math is often not so interesting in its own right, the framework has a somewhat ad-hoc flavour or is oriented towards a rather specific application, proofs may largely consist of crunching relatively trivial subcases etc. And crucially, few people are likely to be willing to digest these proofs in ten or twenty years' time.

Otherwise, the code will bitrot, for example. From what I'm hearing, Lean might be particularly bad when it comes to moving fast and breaking down things, but this problem affects Coq too. Libraries get obsolete. Plugins and tactics evolve. There is not so much effort in making various community developments play nicely with each other, not even comparable to Isabelle's Archive of Formal Proofs.

And this is just within *one* ecosystem, not to mention combining developments in different proof assistants. How many people today can code in and work with, say, Coq, Agda, Isabelle, Mizar, Lean, Abella, Beluga, Dedukti, Twelf, Matita,  Nuprl/RedPRL, and Idris at the same time?!

If you cannot even re-run legacy code in ten or twenty years' time, how about reproducibility of scientific results? And more importantly, how about their reusability? What kind of insights researchers who come after you are supposed to get? How can they check if your proof applies in a modified set-up?

These are increasingly serious problems that, at least in my view, are not sufficiently often discussed or taken seriously by authors and referees alike.

I had other comments on this discussion, but they're best left to a separate email, this one is already growing too big.