The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

I often feel that nowadays some people take offense too quickly and
see racism/sexism/etc. where it isn't.  But it's nevertheless true
that some things really are problematic, and I think it's clear that
the name "Coq" is one of them, whatever the original intent may or may
not have been.  It's probably impossible to be sure that a name won't
have some undesired connotation in some language, but that shouldn't
prevent us from avoiding such connotations when we can, especially
regarding very widespread languages (especially in academia) such as
French and English.  And while ordinary words like "bit" (and, in the
other direction, "clivage" for structure on a fibration) could, at
least in principle, be translated carefully into other languages to
avoid undesired meanings, the same is not true of proper names like
Coq, which are generally not translated.

I would also like to particularly thank the people, particularly
women, who have spoken up publicly to share their uncomfortable
personal experiences arising from the name.  That isn't an easy thing
to do, and I have a lot of respect for those who are able to do it.
Moreover, we should keep in mind that because sharing such stories is
difficult, the number of people who have shared them is likely to be
only a fraction of the number of people who have had similar
experiences.





On Tue, Apr 6, 2021 at 10:44 AM Stefan Muller <smuller2 AT iit.edu> wrote:
>
> 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
>
>
>
>