The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Thanks for pointing this out: we do indeed use Coq at Galois, but we wouldn’t want to make it sound like we are claiming credit for it. :)

Plus, we have built a number of other theorem provers at Galois…

-Eddy

On Apr 6, 2021, at 5:38 PM, Jay Kruer <j AT dank.systems> wrote:

"The Galois theorem prover" has a great ring to it, but I wonder if it might suggest association with a certain defense contractor (https://galois.com/about/) which happens to make use of Coq in some of its projects ;)

On Apr 6, 2021, at 5:18 PM, Joyal, André <joyal.andre AT uqam.ca> wrote:

Dear all,

To add my grain of salt.

The cock became the symbol of Gaule during Roman time

because the roman name for a cock is gallus, which is

close to gallois, the name of an inhabitant of Gaule.

Galois is also the family name of Evariste, a famous mathematician.

I propose to replace "Coq club" by "Galois club".

AJ

---

De : coq-club-request AT inria.fr <coq-club-request AT inria.fr> de la part de Andrej Bauer <andrej.bauer AT andrej.com>
Envoyé : 6 avril 2021 19:58
À : Coq Club <coq-club AT inria.fr>
Objet : Re: [Coq-Club] Why is the Coq logo made to look like a penis?

 

Dear all,

In 2005 I lectured at a logic summer school in Fischbachau, Germany.
Apart from the lectures there were also student presentations, several
of which were about the students' work with Coq. None of the students
ever pronounced the word "Coq". They referred to it as "cee oh que" or
"the French word for rooster", or  "the proof assistant whose name is
on the slide" etc. From what I could gather, this was some sort of an
in-joke, as there was a lot of smirking and giggling going on. Perhaps
some of those students are here with us today and can tell us why they
did it.

I join Michael Shulman in expressing thanks to all who actually dare
relate publicly uncomfortable personal experiences. Their service to
the community is invaluable.

With kind regards,

Andrej