The Coq mailing list

[Derek Dreyer <dreyer AT mpi-sws.org>]

I second Andrew's proposal of adopting "coke" as the preferred English
pronunciation.  I don't relish the association of mechanized proofs
with a sugary soft drink or addictive drug, but it's better than the
alternative.

As for the primary concern of the OP, I trust the Coq team to take the
comments in this thread under advisement and work to develop a better
logo.

Thanks,
Derek

On Tue, Apr 6, 2021 at 5:14 PM Andrew Appel <appel AT princeton.edu> wrote:
>
> Some people I have worked with, Americans who are uncomfortable with the 
> word, pronounce Coq in English as "Coke".   At the time (several years ago) 
> I thought this was silly.  Why did I think so?  Because it's neither the 
> French nor the English pronunciation of Coq or cock, and anyone pronouncing 
> it that way is clearly employing a euphemism to avoid discomfort.
>
> In light of this week's discussion, I would say that it's not silly to 
> avoid discomfort;  especially when the subject of the discomfort is 
> entirely irrelevant to the topic of discourse (which is, in this case, 
> interactive theorem proving using a dependent type theory); and especially 
> when the discomfort falls primarily on one group of people (in this case, 
> anglophone women).
>
> So I propose a solution for discussion:  keep the name Coq and explain that 
> the correct pronunciation in English of the tool name is "Coke" (and this 
> pronunciation has nothing to do with the pronunciation of coq in French or 
> cock in English).    But for this solution to work, the whole (anglophone) 
> community has to adopt it.
>
>