The Coq mailing list

[Vincent Archambault-Bouffard <archambault.v AT gmail.com>]

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