The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

> I think that _if_ there is a new logo, it should not
> be designed by a computer scientist hobbyist, but by a
> professional logo designer.  My two cents.  Surely INRIA
> has some money for that?

Yes. As I already mentioned earlier, getting a new logo was already
planned before this discussion happened and we do have some money to
allocate to this matter.

> As for the name, I think it would be good to undo Huet's
> rowdiness, but it's surely too late for that by now.
> But maybe it's proper to have some apologetic text about
> this issue in the introduction of the Coq manual?

Just to clarify: the explanations that are routinely given about what
the name means / where it comes from (COC, Coquand, French animal,
etc.) are all correct. It just happened that in English, the word cock
has lost its original meaning and got a more common slang one and
Gérard Huet was aware of this. It's not the *reason* why this name was
chosen.

Now, we can certainly regret this choice given the importance that Coq
has taken today and its consequences (this is what I did earlier, and
I know I'm not the only one to do so). But apologize for it? Is a
public statement that this was a bad joke going to make things any
better with regards to the feminization of the Coq community?

Le mar. 6 avr. 2021 à 15:29, Freek Wiedijk <freek AT cs.ru.nl> a écrit :
>
> Dear all,
>
> Now that I have accidentally put something on the list
> after all, let's chime in:
>
> >I happen to agree with Beta's comment (in another branch of this
> >growing tree) that the logo should be as simple as possible in order to
> >work well at various sizes and resolutions. So while the "mechanical
> >rooster" looks nice, I'm not sure it's a good choice as a "brand logo".
> >Just look at the level of detail in modern (high-value) brands.
>
> I think that _if_ there is a new logo, it should not
> be designed by a computer scientist hobbyist, but by a
> professional logo designer.  My two cents.  Surely INRIA
> has some money for that?
>
> At least, if we think Coq is important enough for this.
> It's only an academic system after all.
>
> As for the name, I think it would be good to undo Huet's
> rowdiness, but it's surely too late for that by now.
> But maybe it's proper to have some apologetic text about
> this issue in the introduction of the Coq manual?
>
> Freek