The Coq mailing list

[Ian Shillito <Ian.Shillito AT anu.edu.au>]

Hi all,

About changing the logo: it would not be a big problem I guess. I have to say 
that I personally did not see a phallic shape in Coq’s logo before some of 
you mentioned it. While I’m still struggling to see it as obvious, I can 
understand that the conjunction of both the word and the logo can lead to 
this perception. 

About changing the name: It sounds as if the motivation for this change is 
mainly related to an educational context. If so, wouldn’t it be thinkable to 
start an English course introducing Coq by saying something like: 

“This semester we will study the ITP “Rooster”, which is the English 
translation of the French word “Coq”, the original name of this ITP.” 

This sentence is certainly not perfect, but could do the trick as it simply 
states the convention that in the course we use the translation of this 
French word, without mentioning the reason for it (i.e. the name can be 
perceived as problematic). For the ones who did not see straightforwardly the 
link between Coq and cock, they might never make the connection. Afterwards, 
you can use Rooster as you which, without creating any sort of embarrassment 
in the context of the course. 

Best, 
Ian



> Le 6 avr. 2021 à 20:59, Théo Zimmermann <theo AT irif.fr> a écrit :
> 
> Hi Zoe,
> 
> Not really. The introduction was simply entirely rewritten and
> simplified. We could reintroduce Gallina in the sentence "The first
> part presents the specification language of Coq, that allows to define
> programs and state mathematical theorems." (which would become "The
> first part presents Gallina, the specification language of Coq, that
> allows to define programs and state mathematical theorems."). Or we
> could put even more emphasis on it that there used to be by changing
> the first sentence to "This is the reference manual of Gallina / Coq.
> Coq is an interactive theorem prover and Gallina is its specification
> language.". This was the kind of thing I was thinking of when asking
> my question earlier.
> 
> Théo
> 
>> Le mar. 6 avr. 2021 à 11:55, Zoe Paraskevopoulou
>> <zoe.paraskevopoulou AT gmail.com> a écrit :
>> 
>> Relevant to this discussion, I would like to point out that Gallina (which 
>> was a nice alternative name to use) is no longer mentioned in the 
>> reference manual as the official name of the specification language of Coq 
>> (https://coq.inria.fr/refman/ vs 
>> https://coq.inria.fr/distrib/V8.11.2/refman/), which is confusing.
>> 
>> Was this a deliberate decision? I would like to see Gallina in the front 
>> page of the manual again.
>> 
>> Best,
>> Zoe
>> 
>> On Apr 6, 2021, at 12:04 PM, Derek Dreyer <dreyer AT mpi-sws.org> wrote:
>> 
>> Personally, I would support changing the name *and* the logo.
>> 
>> The root problem is the name -- I rather doubt the logo would be
>> controversial if it were not for the name.  As is well known, the name
>> was deliberately intended partly as a joke, to provoke people -- it
>> has succeeded in that regard.  But mostly at this point it is just
>> embarrassing to a lot of us, and probably exacerbates the gender
>> disparity in Coq users.
>> 
>> I have heard people say that it is hard to change the name.  I agree,
>> it is hard, but that doesn't mean IMO that it's not worth exploring.
>> I bet that many Coq users would be very open to a name change if a
>> catchy new name were proposed by the Coq team.  I would, for one.
>> (And I'm happy to help brainstorm about new names privately if anyone
>> cares to have that discussion.)  Of course, perhaps I am wrong: it
>> might be worth polling Coq users about whether they would like to see
>> the name changed, if that has not been done already.
>> 
>> That said, if there is not sufficient support for changing the name, I
>> would at least support changing the logo to something that is less
>> open to interpretation and more clearly resembles a normal rooster (or
>> even Ilya's steampunk rooster).
>> 
>> Best regards,
>> Derek
>> 
>> 
>> On Mon, Apr 5, 2021 at 6: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
>> 
>>