The Coq mailing list

[Stefan Muller <smuller2 AT iit.edu>]

I was hesitant to chime in on a discussion that already has so many voices, but feel like perhaps this is one area where having a lot of voices from different perspectives is good. I will also clarify how my perspective is and isn't useful: I'm very much an outsider in the Coq community and don't really feel I have sufficient stake in a name (or logo) change to strongly advocate one way or another because I wouldn't be the position of having to, or being able to, do the work to make that change happen. Nor am I a woman, and hearing the (first and second-hand) experiences of the ways in which this name has caused problems for several women Coq users and potentially prevented many others from becoming Coq users has been eye-opening and shifted my thoughts on the issue.

To the extent that the perspective of an infrequent and casual Coq user is useful, I have found the name to be an inconvenience and embarrassment. It changes the way I can talk about my work in public settings, and it hurts my teaching. I'm currently teaching an introductory programming languages class and wanted to bring up the example of Coq on the first day on a slide showing type systems of various degrees of expressiveness. Like Jay, I generally take the approach of making my best attempt at a proper French pronunciation (I suspect many on this thread who are not offended by the name would be offended by my attempt at speaking French) so as to at least make it noticeably different from how the English word would be pronounced, and hope that this, together with giving the spelling on the slide, gets the message across. I could have said "C-O-Q" but we know that that's not how it's pronounced and people will inevitably stop pronouncing letters in acronyms. I also don't have the luxury in such a setting of being able to delve into Coqand and the calculus of constructions.

So, as a male outsider, I would be more likely to discuss my work in Coq and more likely to bring it up to undergraduates if I woke up tomorrow and the system magically had a different name. If many others are in the same position, I suspect that alone would make a name change a good thing for the Coq community and for science in general. (Does that alone make the work of a name change worth it? Like I said, as an outsider, not really my call.) If, as has been credibly shown, the name is hindering the broadening of the community and causing problems for members of the community, that is an even bigger problem. I'm not generally one to clamor for changes in historical names due to cultural shifts (we can have that argument off-list, though I'd rather not), but I don't really think many of those arguments apply here, especially if the discomfort of the name was intentional to begin with.

Those are my two cents. Now back to searching for public domain images of baby camels to put in my compilers homework assignment about the small language "MiniCaml" (see, INRIA, I like some of your names!)

Stefan

Stefan Muller
Gladwin Development Chair Assistant Professor
Computer Science Department
Illinois Institute of Technology

On 4/6/21 11:36 AM, Yao Li wrote:

      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