The Coq mailing list

[Cyrus Omar <comar AT umich.edu>]

The first sentence on the About Coq page [1] says "Coq implements a program specification and mathematical higher-level language called Gallina".

If that is accurate, then I think Gallina seems to be the appropriate name to use in conversation as a user of the language, in the same way that one says "I write C programs" even if what they are doing day-to-day is interacting with GCC, Clang, or CompCert via a collection of other utilities, e.g. editors, language servers, and the like.

The objection that Gallina is one of several languages associated with Coq is the same as the objection that in fact there is a C preprocessor language distinct from C the language, i.e. not salient in most contexts.

There may still be reason to rename the Coq implementation of Gallina (and friends), but it would make it less urgent in that it is only in relatively sophisticated company, where crude innuendo is increasingly (though not yet universally, I concede) recognized as inappropriate, that one needs to mention which particular implementation of a language they use or work on.

Cyrus

[1] https://coq.inria.fr/about-coq

On Tue, Apr 6, 2021 at 8:34 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