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 :)

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?

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.

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.

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.

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.

> 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 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.

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

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.

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.

> 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?

> 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.

> 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

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.

We used to have a sense of humor, too: https://en.wikipedia.org/wiki/Cox%E2%80%93Zucker_machine

Richard Holder and Michael Hunt would be so jealous

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.

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).

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

Is there any evidence of this?

I can easily imagine authors making that decision voluntarily.

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.

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.

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.

yet us french people have exactly zero problems with "bit" sounding the same than https://en.wiktionary.org/wiki/bite#French

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.

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.

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.

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.

like they'd never teach you how to make coq au vin in culinary school.

Coq a l’ordinateur

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.

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?

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.