The Coq mailing list

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

Hi,

I'm afraid I have here (as one of the moderator of the list) to remind
some healthy basic « rules of conduct ». The Irish words I just read
go beyond what is welcomed on the list, whatever one may think of
Conor's fragments of words.

I find otherwise quite interesting matter for thinking in the rest of
the discussion.

On the constructive/classical debate, I tend to think that it is
indeed a rather ideological issue. I would not be surprised that by
about say 5 years from now on, we are able to design a type theory
with fully-computational excluded-middle and fully-computational
extensional axiom of choice. Presumably, this "classical" type theory
will build on a cubical equality, which, I agree here with Thorsten,
is the nicest way I know to provide computational quotients. Moreover,
on the practical side, it would be easy in Coq to provide as soon as
now a file axiomatizing quotients, as Arthur proposed, the same way as
classical reasoning is already supported axiomatically.

While I'm at technical questions. I was pretty interested by Kevin's
question about working in a system "which will instantly know that a
totally ordered field is an additive group or that if R->S is a ring
homomorphism then any S-module is naturally an R-module". I believe
that there is more to say about this important point.

And while I'm at writing, let me thanks, like Théo already did, Bas
for initiating this discussion and everyone to contribute, and to
notably thank Kevin for sharing his thoughts in a way worth its
talent, repairing the tone adopted in some decried talks. In
particular, I appreciated his invitation to come and chat at
https://leanprover.zulipchat.com/. 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). I'd like also that we are able
to address the needs of mathematicians as they are, so that proof
assistants eventually deserve being also qualified as mathematical
assistants.

Hugo

On Sat, Jan 11, 2020 at 02:26:31AM +0100, Tadeusz Litak wrote:
> 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.
> 
> 
> 
>