The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

There is indeed an interesting thread on this topic on the Coq Zulip:

  https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Quanta.20Magazine.20article.20on.20formalized.20math.20libraries

Here were my main takeaways:

- The main point of the Quanta article is to sell proof assistants to mathematicians.

  Quanta (I learned in this thread) is well-respected in the mathematics community.

- The article is fairly negative towards Coq, but this is a minor aspect of it compared to the main point.

- The journalist that wrote the article contacted some people in the proof-assistant community,

  without telling them precisely what the article would be about, and without getting them to read

  the whole piece to see their quotes in context. Given the honesty and frankness with which

  members of the academic community criticizes its own work, it's easy to get quotes to align

  with a narrative created for the article. (I haven't read the article, but it sounds like

  the narrative is that Lean is the new, best tool around, finally solving mathematicians'

  real problems, while the other proof assistants are old and crufty).

- Coq would benefit from better publicity outside its user community.

- There is now interest in proof assistants outside its early community, so we are going

  to see more general-audience articles about them. Many of them will be frustrating!

The other takeaway is that Zulip is a reasonable place for conversations to happen, and indeed there are many interesting things on the Coq Zulip (and the Lean Zulip, and the category-theory Zulip, etc.).

Personally I think that it's hard, and probably a waste of time, to argue with facts that are put in the wrong context but mostly reasonable (there is some cruft in Coq and its ecosystem, Lean is in many ways a cleaned-up version whose design benefited from a fresh start, there is a nice momentum and excitement about mathematics in the Lean community). I think it's more effective for the Coq community to:

1. Advertise its own strengths (rich, diverse ecosystem (including excellent mathematics libraries), a remarkable open development process, its rich history, its no-built-convenience-axiom flexibility, etc.). Communicating this better may not be too hard, but it's not the strong point of most people around here.

2. Continue making progress on alleviating its weaknesses, and interacting in positive, productive ways with other proof-assistant communities to benefit from their work (stealing nice-dependent-pattern-matching from Agda, performance-engineering ideas from the Lean implementation, why not a cleaned-up tactic language, etc.), and help them benefit from Coq's advances. This a lot of hard work and already actively worked on.

On Sun, Oct 11, 2020 at 10:16 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Sun, 11 Oct 2020 20:46:51 +0200
Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

> see zulip

So that's where the party's at.  I've been hanging out in the wrong bar.

>
> Gaëtan Gilbert
>
> On 11/10/2020 19:44, jonikelee AT gmail.com wrote:
> > https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/
> >
> > About Coq, it says:
> >
> > Coq users have formalized a lot of mathematics in its language, but
> > that work has been decentralized and unorganized. Mathematicians
> > worked on projects that interested them and only defined the
> > mathematical objects needed to carry their projects out, often
> > describing those objects in unique ways. As a result, the Coq
> > libraries feel jumbled, like an unplanned city.
> >
> > “Coq is an old man now, and it has a lot of scars,” said Mahboubi,
> > who has worked with the program extensively. “It’s been
> > collaboratively maintained by many people over time, and it has
> > known defects due to its long history.”
> >