The Coq mailing list

[Marie <kerjean AT lipn.univ-paris13.fr>]

As a french speaking new user of Coq, I would just like to point out
that the discomfort due to the name of the proof assistant is not
limited to english speaking users: English is the language employed
internationally at any conference. I avoid mentioning the explicit name
of the proof assistant I'm using when speaking to academic from other
domains, so that to avoid the inevitable grins and jokes.

Marie


On 06/04/2021 17.53, Jakob von Raumer wrote:
> I don't know how you can file this under "political correctness",
> Thorsten. The term usually describes adaptation of ones language or
> behaviour to appeal to some ruling class or in-group. I think the
> anecdotes shared here make it clear that this is not at all the
> motivation behind questioning the name.
> 
> I also count several voices in favour of renaming -- or changing the
> pronounciation -- from people who are definitely working outside of the US.
> 
> On 06/04/2021 17:37, Thorsten Altenkirch wrote:
>>
>> I wonder whether there is a bit of cultural imperialism in this. I
>> have noticed in the past that US researchers are always very outspoken
>> when it is about political correctness issues like this. After all coq
>> was developed and named in Europe and maybe it should keep a name
>> which is European and not Americanized.
>>
>>  
>>
>> *From: *<coq-club-request AT inria.fr> on behalf of Stephanie Weirich
>> <sweirich AT seas.upenn.edu>
>> *Reply to: *"coq-club AT inria.fr" <coq-club AT inria.fr>
>> *Date: *Tuesday, 6 April 2021 at 16:22
>> *To: *"coq-club AT inria.fr" <coq-club AT inria.fr>
>> *Subject: *Re: [Coq-Club] Why is the Coq logo made to look like a penis?
>>
>>  
>>
>> 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 <mailto: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 
>>
>>  
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please contact the sender and delete the email and
>> attachment. 
>>
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored 
>> where permitted by law.
>>
>>
>>