The Coq mailing list

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

On 11.01.20 01:38, Conor McBride wrote:

Ah, poly.

Póg mo thóin.

Now for this claim:

"Dear mathematicians: your life will be the same as it is now, except that faulty proofs will be less common. The only price is, you need to revisit your notions of LEM and AC." I dunno man, hard sell.

This indeed amounts to underselling constructive mathematics.

Look for example at "Models for smooth infinitesimal analysis" by Moerdijk and Reyes.  As another selling point, consider 

http://math.andrej.com/2006/03/27/sometimes-all-functions-are-continuous/

https://arxiv.org/abs/1502.03621

Going around and telling people that  they shouldn't do this or that... and they might be able to prove some of results they believed to have been proved anyway if they try hard enough... is indeed hardly a winning proposition. But, as Albert Visser likes to put it, more is possible in the constructive realm than is dreamt of in classical philosophy.

Regards,

t. [2/3]

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.