The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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