314 comments

[ 5.2 ms ] story [ 306 ms ] thread
Context?
I'm guessing the phallic connotations?
From the link:

>We wish to thank everyone that participated in these discussions. Testimonies from people who experienced harassment or awkward situations, reports about students (notably women) who ended up not learning / using Coq because of its name, were all very important so that the community could fully recognize the impact of the current name and its slang meaning in English, especially with respect to gender-diversity in the Coq community.

Yes, which discussions are those? The link explains nothing.
> especially with respect to gender-diversity in the Coq community.

Seriously there are some people getting shocked that a foreign word sounds like slang for male genitals in their language?

These people seriously need to grow up and accept that not everything is centered around their world.

"bit" is slang for cock in French, "chat" is slang for vagina, "Nike" means fuck, should we rename these so that it does not shock anyone? Where's the limit?

Coq means rooster in French. Unfortunately it also sounds like "cock" which is a word people apparently can't handle in 2021...
Maybe I'm misunderstanding the tone of your comment, are you suggesting that we don't rename things that lead to people feeling unwelcome in a community?

EDIT:

Turns out I was misunderstanding the context; I misread it as something like "look how offended these people get omg", but in reality it looks like the poster was saying that it's sad that we live in a world where this might need to be changed [1]. Entirely my fault!

[1] https://news.ycombinator.com/item?id=26739571

I think it's going a bit far to put it on "unwelcome" just by a name that was selected in another language. But I do get the marketing issue for English speakers with it sounding like cock and of course some people feeling uncomfortable using the name.
Ironically _Code of Conducts_ adopted by many projects nowadays for this very reason also is frequently shorted to CoC which creates the same problem.
FWIW, I read the comment as suggesting it's sad that the rename is needed, rather than suggesting it's sad that the rename is happening.
Pretty much, yeah.
Ah, sorry, I misunderstood. I amended my comment.
You are misunderstanding the meaning not the tone. The OP is lamenting that the bar for "feeling unwelcome" is being lowered. Not that unwelcoming language is being removed.
Problem is that this decision is extremely anglophone centric. Nobody is calling for the Verge to rename because it is an unwelcoming name for French. (It means penis)
Embarrassing people away from reading the Verge is doing them a service.
That's a transparent attempt at concern trolling.
And cock means rooster in English. And of course the slang usage.
We call them 'roosters' usually. Source: many of my neighbors.
You probably call peacocks peacocks though, even though the "correct" collective name is peafowl.
Nope, we don't have any fowl here other than domesticated chickens and the occasional wild turkey family. Also Wild Turkey.

The word "peacock" is now only really useful in streaming TV.

It has become more common to say rooster in recent times, sure, probably because of the slang usage.

Fun fact: Rooster Rock in Oregon looks nothing like a rooster, because it was originally Cock Rock. Because that's what it looks like, and even the Indians named it for that.

Will lecoqsportif.com be next?

I remember childhood-me finding that name quite amusing.

Of course I'm much too grown up now to find it funny....

Because it sounds like cock, one would assume. There’s the same joke in biomedicine around an important family of inflammation genes named Cox1 and Cox2.
(comment deleted)
I'm so glad this is happening. I've tried to occasionally propose we use a theorem-prover at work for stuff that "isn't allowed to make mistakes", and I'm always hesitant to recommend Coq because the name will, at best, get some chuckling and jokes, and worst make people feel a bit uncomfortable.
You could always pronounce it as /see-oh-kju/.
Sure, I could do that, but a lot of the lectures online pronounce it like "cock", at least when the lecture is from an American or a British person.

It it immature to worry about that? Sure, people probably should grow up at some level, but the fact is that I don't really have a magic wand to automatically change the maturity level of every engineer I might ever work with, and those engineers can as a result use it to make people feel unwelcome in tech.

> a lot of the lectures online pronounce it like "cock"

Wow, I discover now that it is supposed to be pronounced more like coke

At that point, we’re already changing the name, so why not go all the way?
Not really. Basically not at all. In bibliography I bet few, if any, times Coq's pronunciation is mentioned. The only thing changing will be in presentations and conversations where the name is a problem.
The vast majority of my communication is verbal, and that includes technical communication. "Only" isn't really "only."
Not sure what's the problem then as, based on that, changing just the pronunciation should be fine.
What about saying "coqlang", similar to golang for Go? Does that still sound offensive? I'm wondering if there would be a way to avoid the issue without a renaming.
Reminds me of the similar problem with the machine learning conference NIPS which was renamed NeurIPS (not much of an improvement if you ask me). There were instances of women at that conference also being forced into uncomfortable situations relating to the name. People are dumb.

Edit: I was just thinking of a few other names that I find amusing but I can definitely imagine people abusing:

- Proceedings of the National Academy of Sciences (PNAS)

- Aircraft Incident Data Store (AIDS. This was renamed)

People are dumb as in, guys guffawing at someone saying "NIPS"?

Yeah, immaturity can be insidious. Even I find myself "looking for the joke" sometimes because my team at work is so silly with innuendo. Mostly harmless, but I wish it were different sometimes.

Maybe just rebrand to be pronounced 'coke'?
(comment deleted)
Are we mature enough on the internet for that option?
I don't think that will work. Sort of like trying to force everyone to say "gif" the "right" way.

IMO, the best route forward is to move completely away from coq and towards something else (like their gallus proposal).

Pretty sure that's how it's already supposed to be pronounced.
(comment deleted)
It’s a shame that an innocent French word for a French tool has to be renamed because of how it sounds to English speakers. It kinda reminds me of how kids tease someone with the surname Wang because of how it sounds in English.

But, the tool that originated in France is now a standard tool in a world where the lingua franca (pun intended) is English, and there’s no avoiding that in that environment it sounds like cock. There’s no choice here that isn’t somehow shitty, so it seems like they’re making the best decision.

A shame, but I just can’t teach it in my programming languages class. I can’t stand up there in front of 200 students saying coq coq coq for an hour. I just can’t.
Call it "coke"? Plenty of people mispronounce Latex. Not the end of the world, and easier than a name change.
Isn’t that the same solution? Change the name because of how it sounds? I can’t see how that isn’t a name change.

In fact, on the list of new proposals for a successor name, a few proposals are pronounced “coke.”

Pronunciation is in fact a different thing than changing a name. If someone mispronounces my name, it doesn't mean they've given me a new name. And people that want to pronounce it coq still can.

Like how the correct pronunciation of LaTeX is "lay-tech", while obviously a lot of people pronounce it "latex".

If someone decided to start intentionally pronouncing my name wrong from now on because they don’t like how it really sounds, I’d certainly feel like they were changing my name.

Likewise for just changing the sound to “coke.” It’s a decision that the real sound sounds bad, with a suggestion to change it to a different sound. Same problem, same solution.

If the maintainers decide to change the sound or the spelling, I’ll call it whatever they want. And I’ll be more comfortable presenting it at work if it doesn’t sound like I’m saying cock.

People (usually by their native language) can't all hear and pronounce all sounds equally well.

If you can't reliably pronounce my name and it'll sound like a bad word when you try, then you should say what you can say safely. I don't care enough that I want you nervous or slowing down a meeting. But if you expect me to change my name to what you could say I would not.

You trying your best is okay, you requiring me to lower the bar so you can succeed is not okay.

like they'd never teach you how to make coq au vin in culinary school.
Coq a l’ordinateur
yet us french people have exactly zero problems with "bit" sounding the same than https://en.wiktionary.org/wiki/bite#French
(comment deleted)
Hah! Yes, a while ago I came up with the "fan theory" that the French named Coq as revenge for exactly that:

https://news.ycombinator.com/item?id=26739666

this, or it just comes from one of the original authors' name, Thierry Coquand ?
We _know_ it doesn’t just come from Coquand’s name, because Gérard Huet very clearly said so.
That sounds like a you problem. Also, you could say "the language" for the oh-so-many times(?) you apparently have to have to refer to it during a programming class.
No because you know what happens? Students snicker and ask insincere questions just so they can say coq in class in front of their friends. They record their professor saying coq and splice it together and upload it to their social media feeds. Female students squirm in their seats and become disengaged, counting down the minutes until the class ends.

It’s the same reason I can’t teach brainfuck. There are 10001 languages worthy of class time and these languages disqualify themselves in my opinion.

How old are your students? I'm truly amazed by what you're saying.

As others mentioned, "bit" means "cock" in French, but by the time you learn what a bit is, you're old enough to not laugh at it anymore. And you surely get to use Coq in your studies when you're older than when you learn about bits.

I mean, in France, laughing at your teacher because he speaks of "bits" (cocks) and you're >16yo would certainly make you look like mentally challenged.

16 - 21. With 200 students in a room there are vast disparities in maturity levels.
Why are you trying to teach 16 year olds theorem proving? They're are no situations in which that will ever be interesting or useful to them, so it's no surprise they would be bored and distracted.
I teach a class on Programming Languages at a US university as part of an accredited CS program. The curriculum is what it is. I don't control who takes my class, and I don't restrict access to any student as long as they meet the prerequisites. At the beginning of the semester I get a roster, and I teach them the material.

For what it's worth, the 16 year old are usually the better behaved, as they are advanced students from high school who are beyond their peers in ability. They find the material eminently fascinating and are fully engaged. The ones to watch out for are the 21 year olds.

I personally learned Coq at 14. Who are you to decide what's interesting and useful to 16 year olds?

Bit is a little less niche than coq, which changes things too.
Why not? That would be a great opportunity to model adult behavior for a bunch of teenagers.
On the best of days I can make the students remember one, maybe two important points from a given lecture. The second I say Coq in class, the takeaway from that lecture is that the professor said Coq, not anything having to do with theorem proving.
For those kids, maybe that's a more important thing for them to learn? I mean, so many future encounters will be affected by their ability to not turn everything into crude sex jokes, compared to the number of circumstances where it will benefit anyone for them to know about theorem provers.

Maybe that's a bit too touchy-feely, but from a more ruthless, "only the course material matters" perspective, fine, let the kids who can't get over the name suffer the consequences. The kids who take it in stride will have an advantage. Nothing wrong with that.

It doesn't just affect the immature kids, because the immature kids affect the rest.
To me, the non shitty choice is for people to stop acting like children and having a problem with a word, even if it does sound like cock.
Fighting human nature is rarely a winning strategy.
It's cultural, is it not?
I would not call it "human nature" or give up on changing it, but I agree that changing the name is a quick and easy win compared to changing the context.
And what is the delineation between nature and culture?
If you view everything at a high level then there is no difference, but that doesn't mean we pretend that nature == culture.
I think this is an XY problem. Presumably the goal of Coq is to solve some technical problems, not change human nature. There's nothing wrong with people having a sense of humor and finding things funny. It's a funny sound in English, just like there are probably English words that sound funny in French, and there are plenty of other words we can use instead of trying to enforce a humorless world where people can't have a giggle at a funny word
Imagine being a woman and having to tell people you’re working with cock. It’s funny for guys but it’s not the greatest for gender diversity. They mention in the linked post that this is one of the main driving reasons, not a vague lack of humor.
Would men have a hard time working with a tool called "vag"?

You seem to be infantilizing a lot of women.

> Would men have a hard time...

I mean, yeah, probably. Either through embarrassment or immaturity. Which, granted, isn't the end of the world, but I'd feel the need to qualify it with an explanation every time I mentioned it, and would probably think about switching to an alternative if I had to talk about it a lot.

It's not quite the same situation, but I switched to Glimpse so I didn't have to keep explaining GIMP to non-techies who saw it on my computer and asked. I would however consider that less excusable, since it's not an innocent word in the program's native language in the same way as Coq.

We're not talking about all women or my opinion of women, we're talking about actual women that actually complained about harassment and discomfort, which is the reason stated for the change in the linked article. Besides, it's not "infantilizing" to acknowledge the situation might feel different as a woman in a male-dominated group. You seem to think they should just tough it out because most men wouldn't have a problem with the "reverse" situation, which is a pretty rough take. Men and women's experiences with the opposite gender are not interchangeable.
How does a name generate harassment on its own? If it doesn't, then clearly the harassment is an issue that should be handled on its own.

It is definitely infantilizing to assume that any group can't adopt/use a word if they want, really has nothing to do with genders or anything like that as you seem to assert. Women don't have some unique historical relationship to the word "cock", and even if they did I don't think that would be a great reason. The black community reclaimed the N word, and that word is so extremely polarizing / offensive I'm calling it "the N word"! It's not about "toughing it out", it's about growing up and recognizing that words are whatever you want them to be.

The thread is full of stories like “woman says she works on Coq and gets harassed” or “woman foresees this problem and avoids learning Coq” or “Coq teacher (male or female) struggles to talk about Coq because students are uncomfortable”.

You seem to suggest those people train everybody around them to change behavior.

Meanwhile, every company picking a brand name will do the smart thing and avoid anything ridiculous in any of their target market; yet somehow if this happens in public it’s a scandal.

> You seem to suggest those people train everybody around them to change behavior.

Yes, I would prefer that as well. Instead of indefinitely (and rather defensively) change the names of things that might be deemed offensive, educate people that there are contexts in which they shouldn't give in to their infantile impulses.

I mean, doctors can do it.. SW engineers too, probably.

We are mostly researchers, so this is not so much a language we use as our life's work. This means we talk about it a _lot_, including in public. It's not just about people at work making jokes; it's also about what happens when you leave work and mention what you do in public as a force of habit. It's pretty awful to expect all of us, especially the women in the community, to have to police the behavior of every stranger we encounter who hears us say that we are Coq experts or something similar, and uses that to make jokes at our expense or harass us.
A guy I work with has 'balls' in his name. Yes, he and management expect people to keep their mouths shut.

Anyways, yes we could require him to change his name because it's distracting. That would be one thing to do. It's the solution suggested by people in this thread...

If you can't see the many differences between those situations, I don't feel like we will have a productive conversation.
Both involve expecting people to respect foreigners and their language.

There's a difference of magnitude, in that one is a guy's name and the other is a guy's project's name. But no, I don't see a fundamental difference.

As a man, yes, yes that would indeed make me uncomfortable.
> You seem to be infantilizing a lot of women.

Welcome to 2021. If you're born with one or more of certain immutable characteristics, you're automatically a victim who needs to be protected and rescued. Every person with certain immutable characteristics of a different category are all personally to blame.

There's no analysis of this that doesn't boil down to accommodating immaturity. Worse, it protects English speakers from the mental model (reflecting reality) where other languages coexist with their own.
You have to remember that most of our communication isn’t written, social media non withstanding. Combine that with Coq still being super niche, so a big fraction of people in a given conversation about it won’t know “Coq” and will hear “cock.” What you end up with is you giving a presentation at work about your new cock proof, or teaching your students how to use cock. Because in the environment a massive number of users are in (verbal, unfamiliar, and English speaking), that’s how it comes across. Is it really childish to acknowledge that I don’t want to have to preempt that my cock presentation is actually about the theorem prover Coq again and again and again?
That's pretty much my take on it too. It's a bit unfair to the maintainers that their innocent name is sort of being co-opted by English, and for that matter it kind of sucks that English is the standard language for most scientific writing, but sadly that's just the way it is.
The same thing happened in reverse with the Toyota MR2, which in France was just called the Toyota MR, because "MR2" sounds like a swear word (merde) in French.
Also with Mitsubisi Pajero in Spain. "Pajero" is slang for wanker here.
If you think that's interesting you should see an even worse case that happened recently. During a Champions League football match a Romanian reserve referee was arguing with some folks from one of the teams playing. He wanted the most vocal to get a yellow card. There were multiple folks there, all dressed the same, similar builds.

So, being slightly naive and maybe stupid, he told the Romanian main referee to book "the Black one", in Romanian. Black in Romanian is "negru". And it's not offensive (maybe a bit too colloquial for the setting), we have a ton of offensive words he could have used. Ironically, they wouldn't have understood any of the truly offensive words, I'm quite sure.

Because a ton of the folks around being English speakers you can figure out how this ended.

From a certain perspective you could say it's cultural imperialism.

Reminds me of people on Twitter being outraged because the color of an item was written on its packaging in multiple languages:

Black Negro Nero Preto

Sometimes they aren't renamed, like the Mitsubishi Pajero..
The Pajero was renamed in a lot of Spanish speaking countries.

Still, a lot of Spanish farmers drive one impervious to its slang meaning. This is probably because it actually does the thing they need it for, does it well, and they have better things to do.

I sometimes joke that "Coq" was French revenge for the Anglosphere making "bit" a common word in computer science, which sounds like the French equivalent of "cock".

https://fr.wikipedia.org/wiki/Bite

Even without knowing French, you can kind of make out this part:

« Bite » est une expression d'argot désignant vulgairement le pénis.

I had the same reaction, coming from the perspective of an adult doing paying work. If your engineers can't use a language called Coq without creating a hostile environment, you have a much bigger problem with how they behave around people named Wang, Dong, Mount, or Kuntz. You urgently need to fix that problem.

But, on reading the discussion page, I realized I forgot about kids and students, especially women, and in that context, even though changing the name is obviously not the best or most important way to solve the problem, it could be a great mitigation and is worth doing.

So how should women and kids deal with Dr Dong? Would it make sense to metaphorically pull Dr Dong out and offer some friendly advice about changing their name, one with a better culture fit?
Children will deal with it badly, of course. That's why it is a mitigation, not a solution. Unnecessarily creating opportunities for the problem to manifest will not result in the problem being solved more quickly; it will only increase the damage from it.
Or, to use a personal example: My pediatrician was Dr. Raper. To my recollection, the rather infelicitous nature of his last name never came up in conversation among his patients, although I’m sure the oddity of it crossed some minds...
Semi related, it always bothered me how cool we are with the term “therapist”, even for someone who treats rape victims.
Wow, I don't think I will be able to unsee this.
Not a doctor, but I changed my name in college because even if people are too adult to make fun of the name, they still get an awkward look on their face. Also, professors struggled to mispronounce my name in order to make it sound less lewd to their English speaking ears.
So the whole world has to bend to the US's language/culture. What about the other way, when american words sound offensive in other languages?
The Chevy Nova was famous for its interpretation by Mexicans. In Mexico it means “doesn’t go” which is a less than ideal name for a car.
If it's true that you can detect bad actors by seeing them persistently make inappropriate jokes about Coq in the workplace, then might it actually be a good thing to have something named Coq? Because you can detect them and deal with them early before they do something worse than make dumb jokes. If that works, that sounds useful enough that one might consider deliberately giving something a funky name.

Following that train of thought, given that kids will eventually encounter something that makes them giggle, mightn't it be good for them to do that and get used to being "professional" as early as possible? (Though there's probably an age below which getting them to stop giggling wouldn't work at all.)

Last, considering the case of a male professor that makes sexual innuendo towards female students as a come-on... I don't know how these things work, but is it possible that this would make it easier for the girls to figure out that he's "creepy" and someone they should avoid (possibly even giving him a reputation they learn about before meeting him), thus reducing the likelihood that he's in a position to do something worse? In fact, given today's neopuritan colleges, it seems likely that him doing that might in itself get him fired; or at least it could put him on thin ice, to be more immediately condemned if students start accusing him of doing worse things.

I don't know if the above scenarios would actually happen that way. But I do suspect that the people arguing to get the name removed haven't thought through second-order effects like those.

> and there’s no avoiding that in that environment it sounds like cock

Cock means "adult male bird" in English as well. See: cockfighting[0]

[0] https://en.wikipedia.org/wiki/Cockfight

True, but of the last hundred times you came across the word cock, how many would you say we’re using that meaning? Probably close to zero for a lot of people coming across Coq. You know that meaning wouldn’t matter if you tried to name your new repo at work “cock” as in rooster.
It's a verb too, i.e. cocking a rifle, cocking your head. "Cocky" is also a commonly used adjective. It is an entirely benign word in most contexts.
Cypress Hill: Cock the Hammer
Even innocent English words and abbreviations are getting cancled. kill process is no longer OK. man pages are under fire. There's no way coq is escaping the word cancellation brigade.
I guess you don't find it embarrassing so you don't see the problem. You're probably in the category of people snickering at some young woman made to say "cock" publically and not in the category of people who are made to feel intensely uncomfortable by it.

Names are arbitrary, why should anyone be so attached to this name, or any other name, idiom, or figure of speech that offends, embarrasses or diminishes others? Because historically we've been able to get away with it?

If you don't care that's fine, but please don't sound so hard done by because people are thinking about how other people feel.

> You're probably in the category of people snickering at some young woman made to say "cock" publically and not in the category of people who are made to feel intensely uncomfortable by it.

What a shitty comment.

> but please don't sound so hard done by because people are thinking about how other people feel.

They aren't though. This isn't about the poor (theoretical) coq-sayer, this is about the righteousness of the name decriers. If you can't point to a real victim we're better off assuming there isn't one and that you're just trying to look hip.

> any other name, idiom, or figure of speech that offends, embarrasses or diminishes others?

Sure, if it did actually diminish people someone would take you seriously. If the product was named after a slur, actually referencing it, and rudely. Like "TheMick, a project to track alcoholism".

But who is hurt by the concept that words in one language sound like different words in another? And is the speaker of the first language to blame or the speaker of the second who hears a dirty word? Allocate blame here, that we may smite the wicked.

> I guess you don't find it embarrassing so you don't see the problem

Even if I did I'd be hard pressed to tell some French people that they have to change because of my sexual puritanism. Is the left into forcing America's sexual mores on people again this week?

> in a world where the lingua franca (pun intended) is English

That would be for computing in general. When it comes to proving software, France's academia seems to be one of the few that takes "making working software" as a serious development for the future (maybe because of airplanes and nuclear power plants). They're actually in the forefront here, if not leading.

The correct response to "Coq sounds funny in English" should be:

"Maybe just learn French?".

It comes across to me as quite puritanical.

There's hardly a single word in existence that can't be turned into an innuendo, or sound the same as a rude or funny word in another language.

If you want to reinforce the notion that cock can only mean penis, this is one hell of a way to do it! Meanwhile, cock is a common term of affection in Northern England ("Cheers, cock", although it might sound more like 'cyock') and also features in the name of countless pubs.

It's one of those things that says more about the accusers.

> Maybe just learn French?

Great response, bonus points for having that totally smug tone that could come from a Parisian that had a bad morning.

I don't think they are making a decision, rather being pushed to make a certain decision, that might not necessarily match their view.

I aknowledge English as the lingua franca of our digital world, but that doesn't mean that we should be attached to every aspect of English speakers cultural environments, basically because we have our own environments too, and are just as valid as theirs.

> [they are] being pushed to make a certain decision

Is there any evidence of this?

I can easily imagine authors making that decision voluntarily.

The core team of Coq developers in France has mulled over this for years, but hasn't had enough momentum or interest to push for it. Right now the broader community of contributors and users, myself included, are arguing our points, suggesting name ideas, and attempting to drive some kind of consensus. My understanding is that the final decision will be democratic among users and contributors. Some are projecting weird politics onto this, but the conversation is otherwise proceeding quite civilly and constructively.

Almost all dissenters in the thread (possibly all of them, I don't remember) do not work for Inria, the research institute at which Coq is professionally developed. Though they are community members like me (I am lightly in favor of the change, and I am both a contributor and a user).

On the other hand I am extremely tired of the US' continuous disregard of the existence of other cultures and languages. English might be the lingua franca but the US one is not the "cultura franca" of the whole world. I live in a place/culture where hearing Coq makes me think of the french word for male chicken and only marginally of an English swear word, and I am growing more and more exhausted with this kind of juvenile, sterile thinking.
There's a sporting goods brand called Le Coq Sportif.

There are people with the surname Le Coq.

This Anglo-centrism bothers me as well, because we can find words in English that sound dirty in other languages.

There's also Dick's sporting goods in the US :)
To be clear, this name was chosen by the creator of Coq, Gerard Huet, with the intention of trolling. It wasn't an innocent French word.
This is wrong. The name Coq is a reference to CoC (the Calculus of Constructions) and to Coquand (the inventor of the Calculus of Constructions). Incidentally, it is one of symbol of France. Its meaning in English provided an opportunity for Gérard Huet to troll with the name, but if the intent were to troll, there would have been many other possible names suitable for trolling, no need to choose Coq. And reciprocally, with many different names would have it been possible to troll, if your intent is to troll.
My understanding was that it was the icing on the cake to Huet. I'm still not sure that changes much.
Is there a citation? The literature is upfront about the JMeq joke, by contrast I've never read anything about this topic.

I'm neither English nor French. I've never seen anything else than a rooster in the name or the logo.

In terms of multiplicity of meanings, certainly. Anyway, if you're interested in my personal opinion on Huet's "humour" and how this degenerated, we can talk privately.
In english at least, we call this a “double entendre” ;-)

Obviously the very purpose of double entendres is to troll those who will get the second meaning. duh!

I wish to clarify this comment; what I said above is strictly correct, but several people have drawn an undesirable conclusion from it which leads me to find a clarification necessary.

It is not the case that trolling English speakers was the primary motivation of Huet. My understanding is that the trolling was a side-benefit to a name he would have chosen regardless of whether it evinced the double entendre.

Name it "Rooster". Or "Gallo". Or "Poulet".
Seems like a slap in the face to France.

"Hi, cool tool, but we need to change the name to be Rooster, otherwise Americans will be offended because Coq sounds similar to body part slang (and they can't be bothered to look up the origin of the word despite its curious spelling)."

I think we need to seriously take a look at our word outrage culture. My brother works at Cerner and recently had to drop everything to address a ticket that was prioritized above all other tickets (including patient safety tickets). He had VPs breathing down his neck until it was fixed. The ticket? The spell-checker in one of Cerner's tools suggests the n-word if you happened to misspell something similar to it (for example if you misspelled "niggard", which means stingy person). He literally had to completely remove the word from the spell check dictionary before the VPs were satisfied.

"Sticks and stones" is apparently a deprecated/obsolete proverb in 2021.

> I think we need to seriously take a look at our word outrage culture.

First off, who is "we" in this case? Society? The government? Professors?

I don't really see this as "outrage culture". I haven't seen a bunch of bunch of posts on Twitter saying #cancelInria or anything like that. They merely saw that the name was being used to make people feel unwelcome, and decided to change it.

They are free to name it as they please, but their reasoning is spurious. There was nothing wrong with the original name and if one took it negatively, they seriously have some maturing to do. Are French chefs going to start renaming Coq au Vin? I think not, because the intent of the name is fully understood by English speakers and understood in its context.
It's unpleasant to work with an obscure technology with a name that is internationally recognized as a swear word / sexual. Coq au vin doesn't really compare simply because it is a much more well-known term, and because the 'au vin' part helps anyone who isn't familiar realize you're probably not just using the swear word.

Not to mention, we don't need to debate - the team studied this and discovered that it is causing real problems for real people, even among those who are familiar with the name.

Overall, this all just proves that it's a bad name. It may not be worth it to change it, and it would be absurd to blame or attack anyone for coming up with the original name, but it should be recognized that it's a bad name.

I personally find it nice because its short yet unique and easy to google search (safely, even).
Not that it matters anymore, but I always pronounced it more like "coke" than "cock":

https://youtu.be/bIraCzL3dtI

The closest English approximation is probably “cook”.
Or "cuck"? Depends on the variety of English, I expect.
Here's the logo, for those interested. Honestly it's a bad logo in general, but when you combine the name of the language, the color of the logo, and general shape, it's downright terrible (not even in a harassment sense, in a literal "why should I care about this product" sense).

https://en.wikipedia.org/wiki/Coq

Looks like whoever made the logo thought it would be funny
Quoting the mailing-list (which currently seems down):

> Hugo reminds of us of the history of the current logo, which is a reference to the Barcelos Coq from Portugal which Gérard Huet liked, whose shape was drawn by Julien Narboux and adapted/colored for the website by Jean-Marc Notin.

The story seems legit to me, knowing some of the people. I believe there were no jokes in the logo itself, but could be wrong. This was from a time where research projects had many hand-made logos.

The proposals: https://github.com/coq/coq/wiki/Alternative-names

I particularly like Chapon, if the name was to change (from the announcement: this is not yet a commitment toward a renaming)

A chapon is a castrated cock. That might offend animal rights activists!
(comment deleted)
That page is a goldmine of involuntary comedy. At the end of the day, the more languages you care about, the more likely you are to find some animal-related term that has become sexual slang somewhere at some point.

I understand their predicament and agree it needs a new name though (it’s actually surprising how long they’ve gone before accepting that it’s a problem, in such an anglo-dominated field as computing). I just don’t think they’ll find a solution if they stay “around a farm”... I mean, looking at other names they have, gallina in Italian is a hen, but also a very common negative slang for “stupid woman” - any Italian woman using that language would feel horribly. The whole farm-related imagery is ripe for this sort of thing.

Makes you think that Kernighan and Ritchie chose really well the least problematic name for their language.
thanks, a quick glance brought "coquito" to my attention, and ponder why "cogito" is not in the suggestion list? a nod to French philosopher René Descartes

dubito, ergo cogito, ergo sum ("I doubt, therefore I think, therefore I am")

May I suggest "chkn".

Unmistakably of a poultry origin and with a bonus reference to the chicken and egg problem. Theorem proving and all.

The hardest thing in Computer Science is naming things.
Wow, I didn't even notice what it sounded like.
This isn't a big deal. There's a long history of product names being screened for this kind of unintended confusion - at times this leads to commercial products having different names in different countries, which isn't really an option for open-source software.
Reminds me of the similar problem with the machine learning conference NIPS which was renamed NeurIPS (not much of an improvement if you ask me). There were instances of women at that conference also being forced into uncomfortable situations relating to the name. People are dumb.

I was just thinking of a few other names that I find amusing but I can definitely imagine people abusing:

- Proceedings of the National Academy of Sciences (PNAS)

- Aircraft Incident Data Store (AIDS. This was renamed)

You know I didn't actually see the issue until you pointed it out a few sentences later. All that came to mind was its similarly to MIPS.
I like the suggestion "Capon": a neutered rooster
the same people probably also find reading Kant offensive
Their heart in is the right place, but in placating the PC set, we're giving ground to the cultural imperialism of the English language.

In naming things to make English speakers comfortable, we're implicitly identifying that other languages and cultures are less important.

This battle was lost decades ago. If you read computer science journal articles, what language are they typically written in? What language are your favorite programming keywords like "function", "for", "if", "else", etc.?
I vote canard.

1) French for duck which keeps the with the language history.

2) it’s a loan word into English for unfounded rumor. Which is kind of fun.

3) the second English definition: “small winglike projection attached to an aircraft forward of the main wing to provide extra stability or control” What does a theorem prover do if not provide extra stability or control to our own understanding? (This one’s a bit of a stretch.)

I worked for a company called Mendix. Most US based sales people would pronounce it more like Mendax. We obviously had quite some running jokes within the company, but most employees only realized after a couple of months. I used to wonder at which stage we would get a new name, but that never happened. And honestly, apart from the inconvenient homonym(?) it's a great name :)
> apart from the inconvenient homonym(?) it's a great name

The first thing that comes to mind when I see it is "mendacious" so maybe not.

I used to know a bunch of people at a company named Incipient. It made it onto many lists of worst company names because nobody knows what it means but they do know what "insipid" means. I did work at a company named Revivio, which was mostly funny because it's hard to spell it out without sounding like Old McDonald.

Definitely a case to be made for that. The one time in undergrad where coq came up in a programming languages lecture, I distinctly remember thinking "haha penis".
We had a joke that our PL course is a maturity test, because Coq and Hoare triples come up in the same lecture...