There are several good reasons to call it Coq:

- The person who implemented the first version (?) is called Coquand.

- The french have a tradition of naming their software projects after animals.

- Coq is french for Rooster.

But to be honest, there is a rather persistent tale that Thierry Coquand's advisor, Gérard Huet, did it on purpose to offend his American colleagues who were too "politically correct" for his tastes.

He also named a certain programming language "Caml". This does have a perfect innocuous explanation, but also happens to be the name of a certain cigarette brand. This was in 1985, when smoking started to be banned in many public places...

Coq is French for rooster. Wiktionary has the pronunciation: https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg

It is pronounced "cock" which is (British) English for a male chicken, what an American might call a rooster. Not surprising, as cock is derived from the French _coq_.

The US media machine, picks and chooses when some words are appropriate and when not, depending if it fits their agenda.

How about the name "Dick" ? As in e.g. Dick Cheney ? Why isn't it considered a slur, just like "cock" ? It an elephant in the room no one speaks about.

How about the word "pussy" as in a small cat ? It has been used to report by the news on "Pussy Riot", which has a direction connection to the female genitalia.

I think it might be because of the sensationalist nature of the US media as such and their juvenile handling of anything that's taboo.

Coq has been around for 26 years. The USA is not the world. No one is offended. Be more inconspicuous when trying to bait next time.

Admittedly, a lot of us still giggle whenever Coq comes up. :)

Even the documentation mentions the issue and calls the name "unfortunate." So, it's a valid critique even if we should ignore it in discussions just to be productive. :)

Really, where? I've always heard this was more intentional than unfortunate.

From the FAQ:

2 Did you really need to name it like that?

Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit convention. In French, “coq” means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based.

The name was intentional as they described. The common reception might have also been intentional as a joke of sorts. ;) Anyway, there was a page or interview where a rep called it "unfortunate" without going into detail. The implication in context was that the name's use in Britain or America often distracts from how the tool is used in a given paper. Hence, unfortunate choice of name.

Should've just picked a different animal haha. The name is easy to spell, though.

And also a tribute to Thierry Coquand, the inventor of the CoC.

Yes, that was also in what I read.

I upvoted your original question because it is a legitimate one, whether others like it or not.

I actually have gotten very few odd looks even from non-programmers when pronouncing "Coq" as "cock" _in the proper context_. "Use Coq" would probably yield a different out-of-context interpretation than "For problem X I think we should consider Coq. It allows ..."

I don't think this is much of a problem in practice.

I just refer to Idris when speaking about dependent types. If I talk about Coq, someone will usually make a joke, which is fine as a once off, but if I want to talk about it regularly I can see that being an issue.

The funny thing is that people try to pin this issue on Anglo-Saxon puritanism, when the issue is clearly political correctness. But those are the contradictions in liberal thinking for you.

American rather than Anglo-Saxon I think, and the US has preferred "rooster" over "cock" since the 18th century, have those horrid liberals been oppressing you with political correctness all this time?

I think you're being downvoted not for your question per se, but because the point of the link is not "hey look at this neat tool we made called Coq", but rather "hey look we formally verified C11". Coq has been around for probably close to 20 years.

Side note – "Coq" is chosen because it is based on the calculus of constructions, whose abbreviation is "CoC", and whose creator's last name is "Coquand".

Coq is a cross-language pun, intended to act as revenge for the word "bit".

Sorry you're getting downvoted but you're not alone, I have the same thoughts every time. I just knew bringing it up wouldn't be good. I could never have a verbal discussion about the language. I think that's the reason there's no GIS library written in Coq, even the most mature person couldn't hold back the giggles long enough to get anything done.

The original pronunciation is more like "coke" than "cock" so this shouldn't be a problem unless you really lack self control.

I'm sure there are plenty of English names that sound naughty in other languages, but somehow the people who speak those languages manage to carry on.