The Coq mailing list

[Yao Li <liyao AT seas.upenn.edu>]

I second Vincent here and add my support.

There are many comments on this thread, on Twitter, and other places about how the name/logo makes people (professional users and newcomers) uncomfortable, and how it makes people refuse the learn it. We are not talking about some potential damages so we might debate whether it was actually offensive. It IS offensive and this has been shown by the damages that have already been happening. To do nothing is to allows this sort of things keep happening. If we strive to be a good community, let us not hide head in the sand and let us fix the problem.

I'm going to join the experiment to pronounce Coq as "see-oh-queue” from now on because that’s some change I can do myself today, but I also think only by completely changing the name we would actually fix the problem. The issue does not go away if we just change the pronunciation—it just becomes more implicit. We might think this saves us trouble but it won’t: One day we will see the discussion to change the name again in this mailing list.

Best,

Yao Li

On Apr 6, 2021, at 11:02 AM, Vincent Archambault-Bouffard <archambault.v AT gmail.com> wrote:

I also support a name / logo change.

To know if it’s too late to change the name we should ask ourselves this question : Will there be more Coq users in the future in comparison to today’s number of users ? If we think Coq still has many years to shine as a solid interactive theorem prover, then why keeping this bad joke ? Eventually the new users will outnumber the current ones, so for most of the community it won’t even be a name change ! 

Plus, if we change the name, we get the added benefit that this male-dominated discipline really would have done something tangible to encourage women in computer science. Just this alone is enough to be proud of a name change.

Vincent Archambault

Le 6 avr. 2021 à 11:06, Stephanie Weirich <sweirich AT seas.upenn.edu> a écrit :

I'll add my support to the feature request for a name / logo change. It would make my job easier as a researcher and educator to have a different way to refer to the tool. The current situation is not terrible of course and there are workarounds as discussed here. But that said, a new name would be an improvement.

In terms of branding, I think that Coq is as hurt by its historical name as much as it is helped. Is it a solid tool developed over decades with a stable user community or is it a fresh new platform that incorporates recent advances in type theory, proof automation and engineering? A new name could bring (well-deserved) attention to recent work by the Coq team to modernize the system.

On Apr 5, 2021, at 12:49 PM, James R Wilcox <jrw12 AT cs.washington.edu> wrote:

I had never noticed this before, despite apologizing for the name of the proof assistant to my students for many years. This year, I had a student point out to me the

flesh-colored logo with what looks like a mushroom top

and now I can't unsee it. 

Isn't it time for a new logo?

James R. Wilcox

University of Washington, Seattle