The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Thorsten, read the response where I wrote about being harassed for talking about my work in Coq.

On Tue, Apr 6, 2021, 8:54 AM Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

I don’t think calling a proof assistant coq amounts to harassment, Talia.

 

From: <coq-club-request AT inria.fr> on behalf of Talia Ringer <tringer AT cs.washington.edu>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 6 April 2021 at 16:47
To: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Why is the Coq logo made to look like a penis?

 

Perhaps we just don't enjoy being sexually harassed, Thorsten.

 

On Tue, Apr 6, 2021, 8:39 AM Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> 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> 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.

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.