The Coq mailing list

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

Hi everyone,

Regarding the name "Coq", I don't think its authors could imagine what
importance it would end up taking, and the consequences (discouraging
female anglophones from using it) this choice of name would have.
Otherwise, I guess they would have chosen something else.

As several people said, changing the name now sounds too difficult.
Fortunately, Coq is associated with another name, Gallina, which is
the name of the underlying specification and programming language.
Without changing the name of the proof assistant, we could associate
it with Gallina more systematically if that could help defuse the
joke. What do anglophones (and others) think of writing more
systematically the "Gallina / Coq proof language" / "Gallina / Coq
proof system" / "Gallina / Coq proof assistant" / "Gallina / Coq
prover" in documents without changing any of the package and command
names?

I'm just asking a question here, not committing to anything in
anyone's name. Also, I'm not the one who had the initial idea of using
Gallina as a substitute (or complement) to the name "Coq".

Regarding the logo, as someone already explained, it was not "made" to
look like a penis (and several of us have a hard time seeing it that
way even after this discussion). However, I agree with the others that
if some people see it that way, it's a good reason to consider a new
logo. This was anyway something that many developers wanted, simply
because the current logo is not to their liking anymore.

Changing the logo was discussed last October. See the notes
https://github.com/coq/coq/wiki/Coq-Call-2020-10-07 (which also
contain the history of the logo). Re-using the coq-community logo was
discussed, but decided against based on arguments similar to the ones
made by Christian earlier in this discussion.

The project has not moved forward since, due to issues related to the
ongoing pandemic, but the idea is still there.

Théo

Le mar. 6 avr. 2021 à 10:18, Ralf Jung <jung AT mpi-sws.org> a écrit :
>
> Hi all,
>
> While we are collecting "words commonly used in our community that have
> (un)intended meanings in other languages": when I heard the conference name
> "POPL" for the first time, I thought someone was making a joke, since it's
> pronounced basically the same as the German word "Popel", English 
> "booger"...
> every time I tell non-PL friends and family which conferences I go to, I 
> have to
> explain that one.^^
>
> Kind regards,
> Ralf
>
> On 05.04.21 20:43, Andrew Appel wrote:
> > The English word "bit" was coined by Claude Shannon as an abbreviation of
> > "binary digit".
> > The French word "bit" is a cognate of the English word.
> > The Frech word "mot" is a literal translation of the English word "word",
> > so you can translate "32-bit word" as "mot de 32 bits".
> >
> > The word "byte" was coined by Werner Buchholz of IBM in New York.
> > But French computer science terminology uses the word "octet" instead of 
> > just
> > using the English word "byte".
> > To see why, you can use your favorite translation app to translate "bite" 
> > from
> > English to French.
> >
> > I believe that was (in part) the joke of naming Coq as it is:  it's a 
> > perfectly
> > acceptable word in French, it's a symbol of France itself, as well as a 
> > play on
> > the name of an inventor (Coquand) and the abbreviation of the Calculus of
> > Constructions (coc); and as a special bonus, it makes English speakers 
> > just as
> > uncomfortable as the use of the word "byte" would make a French speaker.
> >
> > By the way, the first computer I used had six-bit bytes.  You can 
> > translate that
> > to French as "octets de six bits", which makes no sense at all!
> >
> > -- Andrew Appel
>
> --
> Website: https://people.mpi-sws.org/~jung/