The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

On Sat, Jan 11, 2020 at 10:43 AM Tadeusz Litak <tadeusz.litak AT gmail.com> wrote:

@Timothy: it seems then there is less disagreement between us and your position regarding paper proofs is less radical than it originally sounded, at least to me. And we share the view that "literate programming" is not quite perfect as means of communication, at least not in its present state. Siddharth expressed this well; and it also seems to me that Agda code might be somewhat easier to read for an outsider than Coq code.

I have a tendency to alarm people with my enthusiasm for change :)

I share all of your practical concerns (usability, version stability, the abundance of languages, and others). I'm optimistic about these matters getting settled, likely by a sequence of enterprising and hard-working students who also share these visions, and perhaps (given recent developments) with help from industry (small at first, but perhaps significant over the next 3-8 years). The Coq ecosystem in particular has made great strides in the last several years. I've been extremely impressed with the progress the Coq team has made towards maturation of the code, ecosystem, and metatheory, in particular. Everyone involved should be very proud.

I also want to thank everyone I've interacted with on this thread. We live in really exciting times and it's been an inspiring way to start the year. There's so much to think about!

All my best,

-t