The Coq mailing list

[Santiago Bautista <santiago.bautista AT ens-rennes.fr>]

For choosing the new logo, we could do a logo contest, like the one done for the Haskell Language Server logo (https://github.com/haskell/haskell-language-server/issues/694#issuecomment-762701777 ) .

That would be both fun and productive ;)

Santiago

Le 05/04/2021 à 20:29, Jennifer Paykin a écrit :

In my experience, the name (and perhaps logo, though I don't see it myself) does make English-speaking newcomers uncomfortable, especially women, and therefore makes them less likely to want to learn about Coq. If that were true in another natural language I would say that would also be justification for making a change, even if it were not deliberate.

Jennifer

On Mon, Apr 5, 2021 at 11:25 AM Talia Ringer <tringer AT cs.washington.edu> wrote:

It's worth having a new logo for better illustrating the programming
language, but not for accommodating a specific natural language.

I'd be more inclined to agree with this if the original naming weren't a deliberate joke. But I do know from the Coq developers that it was. So this is not so much accomodating a specific natural language, as not doubling down on a joke deliberately targeting a specific natural language.

Talia

On Mon, Apr 5, 2021 at 11:20 AM Yishuai Li <yishuai AT cis.upenn.edu> wrote:

Not until meeting some anglophones have I realized that the name and
logo both resemble chicken, or the slang behind its name. Before that
I only thought Coq might be named after some person (like Haskell).
Still I'm failing to see the logo as other than a chicken (Google
reads the image as "lovely"). I feel natural explaining to people that
"chicken is a symbol of France, and the lack of details reflects
abstraction".

It's worth having a new logo for better illustrating the programming
language, but not for accommodating a specific natural language.

Talia Ringer <tringer AT cs.washington.edu> 于2021年4月5日周一 下午1:05写道：
>
> I've brought this up before in person, too, at the Coq Users & Developers Workshop. I think using a different logo is good so as not to double down on the 1980s joke to troll anglophones, whether or not the resemblance of the logo was intentional (the name was IIRC). Very much for a new logo, and it's a much easier change than renaming a language.
>
> On Mon, Apr 5, 2021, 9:49 AM 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