The Coq mailing list

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

Thanks a lot Gabriel! I'm all in agreement with you. Hugo

On Mon, Oct 12, 2020 at 09:52:18AM +0200, Gabriel Scherer wrote:
> 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.”
>     > >   
> 
>