Renaming Coq | Hacker News Reader

Renaming Coq

sympa.inria.fr

76 pointsingve297 comments

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

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?

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

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

I kinda have a mixed feeling about it :

  - We have something with a localized name (uncommon for a software tool) that bother English speakers

  - The English speaker changed the original poultry meaning to the modern slang by themselves
 
  - We rename it to something neutral and in the alternative names you have ... English propositions, and arguing about it in english

It's like a double win for the English world, almost like a embrace, extend and extinguish strategy.

I hope the tool ended up with a non-english alternative. As I am in "the either everything is fine or nothing is fine" team, maybe I am a little biased on the subject.

Yes, finally! I'm no puritan, but this name is really embarrassing to use and every time you mention it to someone for the first time you have to go "no, no, no! like 'Rooster' in French!". Long overdue!

It would be a shame to not use a French name though. I don't know about Chapon (it's a bit on the nose to have the new name be "Coq, but emasculated"). I vote for "Canard", which would also be sort-of funny in English.

With minor versions up to the next major nicknamed "connard"? As a transitional naming... ;-)

I have no opinion on to change the Coq name or not, but I have to ask: Do you have similar issues when it comes to Git as well and how do you deal with that?

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.

Fair enough, but I'm pretty sure the Stirling Engine diagram was intended to be phallic:

https://en.wikipedia.org/wiki/Stirling_engine#/media/File:Be...

It looks like a plumbus.

The fact that this is an issue tells me how english-centric is the software community! culturally and linguistically speaking.

Why do some folks have to change it's project name regardless of it's meaning in another language? Coq's name wasn't meant to be offensive.

What would happen if the new name is considered an offensive or uncomfortable word in any other language? would that be a good enough reason to reconsider it? Or we only care about english speaking minds?

If coq's team is fine with it, I'm fine with it (maybe they want to have more users and thats a legit reason to change it).

But this sounds like some sort of peer presure to change it.

This is just anecdotal, but one of my professors at university said that the name was intentional, as a joke to make English speakers feel uncomfortable. I've not idea if this is true but it would make sense that the creators of Coq would have been aware of its English translation (lots of people in France speak English, especially in academia).

And it makes sense that it could be intentional. There is a ton of rivalry between France and The US, in cultural terms. French people have a contempt attitude towards US citizen manners, they think they are rude, loud, and often self-centered. When you go to France, don't you dare to speak to someone in English, they are gonna freak out.

I believe it is pretty clever to defy them by using a French word that sounds a little inappropriate in English, if that were the case. Totally legal. But if its not, why should we, non-US Citizens, have to bare linguistic and cultural impositions because some feel 'uncomfortable' with the way we express in our own languages? Totally non-sense.

> When you go to France, don't you dare to speak to someone in English, they are gonna freak out

Please stop spreading bullshit. French don’t "freak out" for being spoken to in English. A lot of people in the older generation don’t have a good command of the language, that’s it. The situation is not very different from a lot of other countries.

ok, I expressed myself wrong. But the fact that tourism leads to tourist tend to speak in English first is outrageous for many locals, old and young, and not just in France.

This happened to me in Germany also, so I started approaching people by saluting them in Spanish, which is my main language, and they had a different reaction (a very positive one) than those who I said hi to in English.

It's not bullshit. Many people have an anti-american feeling in a cultural sense. (not saying I'm endorsing it)

Coq’s name _was_ meant to be offensive to English speakers. And the team does want to avoid names that are offensive in other languages, as EVERYBODY does when choosing international brand names.

> avoid names that are offensive in other languages, EVERYBODY does when choosing international brand names.

This is simply not true. There's plenty of commonly used English names that are offensive in other languages.

I recently saw a tweet of a Ph.D candidate, whose professor asked her 'How good are you with Coq?', and then the prof finally realized what he had said. I think its time to change the name, it might make people uncomfortable.

Honestly, you get used to the name and just kind of abstract over it -- because it's your only option if your work is in the area. It can still be awkward to explain to people what you're working on though, so I welcome the change.

Yes, but I do this so naturally that I often say things like "I'm a Coq expert" when out eating with people I'm close with from my field, and believe me this is not something that works out well for women. People overhear you and at best give you dirty looks, at worst harass you like the driver mentioned in the thread.

I feel you... I'm currently writing my thesis and need to catch myself in time when explaining what I'm doing to people blessed by ignorance. Or alternatively, make the joke right away myself, though that's probably a lot easier to do for me as a guy.

On the other hand, it is kind of hilarious to fall out of your abstraction-tunnel for a moment when citing a source called "A short presentation of Coq".

Anyway, I really feel we need to make at least a few more deliberate puns before they change the name. Maybe just end every sentence referring to Coq in an ambiguous manner with "pardon my French."

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.

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.

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!

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

I've been following this discussion closely because I work in adjacent areas and have dipped into Coq and Agda. Now that I see it on hackernews and all sorts of comments speculating on how this is cancel culture and English-centric chauvinism I'm really disappointed. Sometimes you lack the social context to evaluate the merits of a discussion so you default to your image of the most plausible motivation and it says a lot in this case. A popular idea here is the "gellman amnesia effect", yes? Well I'm definitely not going to forget this in the broader context every time a post comes around baiting culture war rhetoric.

Unfortunately some women actually in the Coq community discussing this on Twitter noticed they were getting all of a sudden a lot more engagement with concern trolls around the time this submission gained traction. "intellectual curiosity" indeed. I hope its worth it, this place existing. I think I can find a replacement though so I'm logging off indefinitely.

Yet 'bit' was never renamed.

This is a sad day for the revenge of french on english.

Is Lean going to be renamed too next ? immature people might mistake me for a proud drug user.

Exactly. This prosternation before american PC is depressing, to say the least.

I'm not sure I've ever heard someone pronounce 'bit' like 'bite' in French. But, in English, everyone pronounces 'coq' like 'cock'.

Bit is pronounced like bite (i.e. cock) in french, Byte is pronounced as in english (although Octet is used too). At least that's how I say it.

It's pretty close but it's not quite the same vowel. Bite (fr) is pronounced [bit], bit (en) is pronounced [bɪt].

But the vowel is also different in cock [kɒk] vs coq [kɔk].

EDIT: I think I missed the point, if I'm reading "32 bits" in a french text then yes of course it sounds exactly like "32 bites".

> if I'm reading "32 bits" in a french text then yes of course it sounds exactly like "32 bites".

My impression in France was that "bite" had the "i" sound slightly longer than in "bit". Some of the pronounciations at https://forvo.com/word/bite/#fr definitely lengthen it, but not all. Unfortunately there is only one recording for https://forvo.com/word/bit/#fr for comparison.

Any difference there is will depend on the individual, and all in all they're pronounced very similarly if not exactly the same.

Seeing 8 GO mobile data plans was really weird the first time.

Then I remembered my telecom classes and we use octets because there's no confusion regarding byte sizes in older differet architectures.

How on earth do you pronounce it then?

Not everyone. I've always pronounced it "coke".

I do. As do all people I know of who speak french as their native language.

Hmm. Definitely non-native here. I wonder if I've misattributed some regional variation.

TBH, I can't really think of any other pronunciation.

In my head, bit's i is more like the one in poutine, bite's i is more like the one in vite.

Plot is another pretty bad one, for the Québécois here...

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.

As the server seems down, here is a mirror of the content: https://clarus.github.io/coq-renaming-emails/

(this is mailing list)

Here are some other links related to the discussion:

* wiki, where anyone can add proposals: https://github.com/coq/coq/wiki/Alternative-names

* chat: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneou...

* forum: https://coq.discourse.group/t/renaming-coq/1264

This should be a case where absence of personal experience should not invalidate other people's experiences. I've never faced any weird reactions to the name (other than a sign language interpreter's confusion), but y'know what? I believe that other people have. It's not a big jump. And it's also not a big jump to rename the project.

"Testimonies from people who experienced harassment or awkward situations ..."

These re-namings always follow the same pattern. Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction.

After the re-naming they are never heard of again.

Coq isn't pronounced like "cock" at all by the French. As a first crude approximation, it is more like "coke".

In the Oxford dictionary, "cock" means "a male bird, esp. a male domestic fowl". There's cockroach, cockpit, cockney ...

So U.S. cultural imperialism wins again.

I'm saying this as a person who had problems with the NNTP "suck" program, so I do understand aversions to names, if they are legitimate.

You're wrong about the pronunciation. It's exactly the same, and not pronounced coke at all. Signed a native french speaker.

> Coq isn't pronounced like "cock" at all by the French.

Yes it is: https://forvo.com/word/coq/#fr

> As a first crude approximation, it is more like "coke".

No it isn't: https://forvo.com/word/coke/#en

I just have to thank you for this website. The pronunciation of Coke by wildlandwoman907 was interesting, and I had to click to hear some other words by this user. Turns out the same day they recorded Coke, they also recorded the words "dirtiest", "pimpmobile", and "experience". I just have to wonder...

https://forvo.com/user/wildlandwoman907/

> Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction.

> After the re-naming they are never heard of again.

Beyond all other corrections, the people complaining here are professional Coq users of both genders.

> These re-namings always follow the same pattern. Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction.

Hello, I'm the woman who chimed in with the story of the Uber driver harassing me. I'm not just a Coq expert (check my publications), but also a contributor to the proof assistant (check my Github). Every year during non-pandemic times I go to France for a week for the Coq Users & Developers Workshop, and I am quite close with the team.

I also hear "Coq" before "cock" when people say either of those words, naturally, since I spend so much time working on Coq. Unfortunately, this means that in public I frequently forget that almost everyone who has never heard of it before hears "cock," and this is what most often gets me into bad situations like in the Uber.

The problem isn't that we are community outsiders; it's that you can't imagine us being community insiders.

Surely the easier and better solution is to just give the driver a one star rating, rather than confusing anyone who has ever heard of coq and missed the re-naming. The costs you are inflicting on the software industry are very large when added up, for no good reason (people have to deal with dumb/ annoying taxi drivers all the time).

If I were the only one complaining, I'd agree (with this being unnecessary---I don't quite see how the cost here is very large). But many women in the community both in the US and in France echo my experiences and concerns, as do many men. I also view it as part of my job as incoming faculty to discuss things that students may feel too vulnerable to discuss themselves.

Also, many on the core Coq development teams at Inria just feel this is bad branding for them at this point, as it inhibits adoption of the tool internationally.

> Dear members of the Coq community,

The Coq development team acknowledges the recent discussions (started on the Coq-Club mailing list) around Coq's logo and name.

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.

I strongly agree it should be renamed if only for the reason that the name usually completely derails any news discussion thread it features in with people discussing why it's called that and making jokes. This happens when talking to people about it as well. It's tiring and distracting and is never going to go away with the current name.

I don't see this as some big PC encroachment. This is Branding 101. One of the first things you should do when you come up with a cool name for your brand is make sure it doesn't mean or sound like anything vulgar in another language. You'd hate for your product to take off and get popular and then realize later its name means "asshole" in Turkish or something. This one seems like a no-brainer to me.

I can't wait until the people on this thread find out what git means in British English.

We can argue about the merits of puritanical mores, but this is hardly the same. It's hard to twist "stupid or worthless person" into sexual innuendo to harass speakers (or listeners).

A word meaning stupid/worthless/bad natured person can only be used to harass people, that's its entire purpose. Besides, the assumption that only sexual insults matter is a US-centric cultural view. That's why it's such a common observation in Europe that in American culture there's no problem with depicting blood and gore but everyone freaks out over nipples, which doesn't seem to make any sense.

The point I'm making here is that it's perfectly possible for millions of adults to use a tool with an offensive name without causing a big fuss and demanding everyone change everything. These constant word battles over software identifiers is toxic and immature.

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

Some people are harassing others over homophones, which is sad, so go watch LPL not even smirk once doing this video: https://www.youtube.com/watch?v=k9VewWKfH_0

What would Peter File say about this?

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

This would be great in all honesty

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

From https://github.com/coq/coq/wiki/Alternative-names

> others getting harassed when they said they were working on Coq

It's hard for me to imagine anyone getting harassed over this, who are these people who haven't moved past puberty but are in a professional environment? Is there any examples of this happening in the wild online?

Looking through the examples, if the problem is that people cannot hear something that sounds like "cock" without harassing people, you probably need to chose a name that sounds nothing like it, rather than just a slight modification. Coquito, PeaCoq, Coqpit, Côq, Coq au vin, Le Coq, Coqorico, Coqueluche, Coque, Coqroach etc all sound too familiar and if the purpose is to stop harassment, none of those would be real options.

Edit: on second thought, I wonder if the people who harassed others over using Coq also harass people who are using Git. Why/why not?

I worked at a FAANG company for a while where a manager would walk in each morning and loudly announce, "Good morning all you motherfuckers."

Professionalism is hardly universal.

My fiance worked at Oracle, and her manager routinely offered to "mushroom stamp" paperwork that was submitted for his approval.

LOL! That's a phrase I haven't heard in awhile.

Urgh. That’s immediate dismissal from his post and a brisk escort from the building for gross misconduct in my book.

Flat out disgusting, not to mention illegal.

Well, people talk differently, that's not too bad.

I'm talking about the harassment part here, not professionalism in general.

It became a blanket approval to address anyone on the team as a motherfucker.

Sure, one crass dude is one crass dude. One crass manager sets the tone for the team.

Pretty soon people starting pushing the boundaries on how insulting they could be.

True, and I understand how that can be bothersome for some people. On the other hand, I'd rather have someone that swears like a sailor but is otherwise a decent human being when it comes to the things that really matter (i.e. not imposing undue pressure on you, compassion, treating your fairly even in the context of a frayed relationship (firing, etc)).

To me "professionalism" doesn't mean anything. Just try to be good. Be on time, not because it's professional, but because wasting other people's time is disrespectful.

My problem with "professionalism" is that you can be "professional" by not swearing, wearing a nice suit and never raising your voice - but still being a complete asshole (in particular when the going gets hard). I've met people like that.

I feel like there's hardly any correlation between swearing and "decency" (acting like a good human being). In fact, there might even be a slightly positive correlation, since people will tend to cut you much less slack for such egregious behavior (unless you are at the very top of the chain, I suppose).

There have actually been studies that show a positive link between profanity and honest behaviour/integrity[1]

The study I've linked below is slightly flawed, but it does provide a small nugget of evidence to your anecdote.

[1]: https://www.gsb.stanford.edu/sites/gsb/files/publication-pdf...

I agree, professionalism isn't necessarily a mark of someone who is a good work partner. Professionalism doesn't imply compassion at all.

But also, some folks (for reasons that may or may not resonate with others) might not enjoy working in an environment where they are called 'motherfuckers', 'little shits', etc.

I agree, and this kind of insensitivity is specifically harmful to inclusion efforts. It’s not so much that people in underrepresented groups (women, POC, trans, disabled, etc) are necessarily more sensitive to all crass or unprofessional language. But it can foster an environment where people are comfortable saying inappropriate things, uncomfortable being challenged, and have enough power that addressing it is or feels too risky for anyone who finds it hurtful or offensive.

All that said, I think a good balance is

1. Embrace a level of crassness that feels friendly and comfortable for all. In some cases this means very little or no crassness. In most cases it shouldn’t mean anything that would be posted on CollegeHumor or whatever.

2. Clearly set expectations that any such humor is expected to be in good faith, which implies both actively understanding commonly hurtful humor to avoid; and encouraging, embracing and actively addressing feedback when anything is unintentionally hurtful; actively disincentivizing and penalizing bad faith behavior.

All of that said: I personally have no gripe with being called a “fucker” but I’d prefer “motherfucker” not be used in a workplace for pretty much arbitrary reasons. I have no problem at all being called a “little shit” (or any other size of shit). Applying the principles above, if I were starting or growing a group/team/org, on first usage I’d probably invite people to say if it made them feel uncomfortable, or if it would make them uncomfortable had it been said to them. If anyone said so, or even just hesitated, I’d suggest that I’m comfortable with the personal interaction in private but it shouldn’t be a part of public communication for the group or private communication without express consent. And I’d invite anyone who felt that wasn’t being honored to come to me if they weren’t comfortable speaking up.

All of thaaaaat said: my original intent was to end this comment jokingly inviting all of HN to call me a fucker or any size of shit, but I couldn’t think of a way to do it and allow downthread discussion without contradicting my own principles. So if anyone here wants to call me names for fun or just to get your rude fix, my email link is public and a pretty quick set of clicks away: profile > personal site > resume

Well some people are just linguistically challenged monolinguals. https://en.wikipedia.org/wiki/Cock_(bird)

Even if harassment isn't commonplace, hearing Coq pronounced can be jarring. It is less than ideal that you need to be mindful of how you use the name of a tool that is the gold standard for a particular niche.

Others posted similar things, but imagine that you're a female PhD candidate and your male advisor asks you: "How familiar are you with Coq?" or "Are you good with Coq?"

Sure, the advisor could have asked "How familiar are you with the theorem prover Coq?" but it shouldn't be necessary to do so.

It seems petty and childish to be considering a name change over this, but it is far from unprecedented (e.g. "Beaver College" changed their name to "Arcadia University" in 2001). Having a more utterable name can lead to more widespread use and discussion of the tool with laypeople.

First of all, you can just correctly pronounce it with oh instead of uh if you don't want it to sound like the slang.

Second, Coq sounds kinda like a slang word in English, so it must be changed; bit is pronounced exactly like the slang word for the same thing in French, but you would be laughed at if you suggest changing bit something less offensive like bigit? For many of us non-anglophones, the creeping English-language supremacy is neither natural and inevitable nor welcome.

If by "correct" pronunciation you mean the French one, the vowel is actually somewhere in between "coke" and "cock". English speakers might hear either word when the French word is spoken.

Next, we all stop referring to the different ends of connectors as male and female. Way to suggestive for adults to use

We prefer plug and receptacle.

> Others posted similar things, but imagine that you're a female PhD candidate and your male advisor asks you: "How familiar are you with Coq?" or "Are you good with Coq?"

Yeah, a bit awkward for about 5 seconds until both parties know what you're talking about, because of context.

Is that what the authors are referring to as "harassment" or where does the whole harassment come from? That's my biggest question here. I have nothing against people wanting it to change, I just want to understand the reasoning behind it, and how even people manage to harass others via a project name.

I think it's instructive that s/coq/git/ , s/(fe)?male// and the situation feels similar to how I felt with git a decade ago.

> It's hard for me to imagine anyone getting harassed over this

I have to wonder if you are male.. I'm a transgender woman, and honestly before transitioning I would have thought the same thing. But that's because I was really lacking in perspective. I didn't know what it was like to be a vulnerable, marginalized minority.. and if you've never been vulnerable and marginalized (like women and minorities are), things like this seem like "no big deal" when they actually are in fact a big deal. You've probably never been threatened by someone in a sexual context, so hearing "cock" doesn't have the same effect on you that it has on me.

I've been shocked by the daily harassment and hostility that I have to put up with now. The jokes people make about me that they think are "no big deal". People can be unapologetically terrible, and yes pre-pubescent level harassment happens all the time, even in professional environments. It's just not something that you can understand unless you've been in that position.

Sorry if I gave the impression that I'm downplaying anything here, I'm not trying to. I'm simply trying to understand how "harassment" comes into play by a project having a "funny" name. If someone simply utters the word "Coq" it's hardly harassment, but instead the authors/suggesters of the change seems to indicate that people have been harassed over the projects name, I'm simply looking for understanding and/or examples of that happening.

And yes, if it's important, I'm "part" of a couple of marginalized groups myself, but I'm not sure how that's important here.

Well you're acting like you understand what they're talking about when they say the word harassment when obviously you don't. I don't either, but with all the harassment I experience on a daily basis, I have no trouble imagining situations that would fit the definition of harassment that could come about because of this name. Acting like you understand this whole situation, and the point of view of everyone involved make me surprised to hear that you are a marginalized person.

> you're acting like you understand what they're talking about when they say the word harassment [...] Acting like you understand this whole situation

No, I'm genuinely asking about what they are talking about. I'm literally asking clarifying questions here in order to find out more. I'm not stating how anything is, but merely wonder and want to learn more.

I do experience harassment as well, but not in the form of hearing "Oh, you use Coq so you must be a cock" every day, which is why I ask how the project name can be used as harassment.

How is any woman supposed to specialize in this language without hearing jokes like "oh she's an expert in cock".. The fact that you're trying to assert your point of view over the people who are actually involved in the situation, and chose to use the word harassment, makes me feel like you don't understand these issues as well as you think you do.

> The fact that you're trying to assert your point of view over the people

What? I'm sorry but we're talking way past each other and seem to be having two different conversations here. I'm inquiring about the usage of "harassment" from the authors of the proposed change, and you take it as I'm "asserting my point of view"?

Please do try to spread flame somewhere else but not here. I'm now done trying to explain myself to you.

Why did you immediately jump into questioning the validity of their use of the word harassment? Do you have any reason at all to doubt their claims?

How am I spreading flame? This is something I feel passionate about because these issues affect my life.

Can you explain the Git thing? It keeps coming up but I've never heard of an English word "git." I looked it up and it seems it exists, but is it common? I've lived in this country for 30 years and have never heard it in a nib-technical context.

It is British English and very common in the UK. That's why Linus claims he "named it after himself". Means bastard or horrid person, basically.

Oddly enough, British people don't go around demanding git be renamed. We know how to handle words having multiple meanings.

Yeah, but sexual words in particular lead to harassment of women by strangers. I'd love to fix society so that this becomes false, but it's not how society currently works.

I'll keep that in mind though if I work with folks in the UK at some point.

You realise men get harassed by strangers too? All the time, about stupid shit, and rare is the day that anything is done about it.

It's really quite self centred to create new problems for the entire world because of a taxi driver. Think about how many people will now have to double search for things, or change scripts, or waste time because they didn't realise new tool=old tool. It's a huge new technical debt being created here. Coq is software, it's been around for many years, so the old name will never die. People will be dealing with half baked renames and duplications forever.

Immature people will find ways to be immature and annoying no matter what - the difference between adults and children is we're supposed to be able to deal with it and keep things in proportion. That doesn't seem to be happening here and it's a pity.

I do not believe you are engaging in good faith, given that I just explained to you very clearly and concisely that this is not just about me.

And yet your demands have contributed to that decision.

Please don't accuse others of "not engaging in good faith" when they just outlined to you the rational basis for their viewpoints. It's just an ad-hominem insult. My engagement is in entirely good faith: I think you (and others making these demands) are refusing to consider the impact of your demands on other people, externalizing costs unnecessarily and generally acting in anti-social ways, whilst claiming the exact opposite.

I didn't demand anything. I contributed my story to a decision that I along with the rest of the community will make democratically.

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.

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

The name surely recalls the same word as the acronym of Code Of Conduct, which I always wondered why are they using that acronym in texts (like "Enforcing a CoC") and nobody is complaining. But then I think it's just because I am a non-native English speaker and perhaps it sounds/reads differently?

I read Code of Conduct abbreviated as "see-oh-see." This is also the name of the logic that underpins Coq, the Calculus of Constructions, which I read the same way.

Site is down http://web.archive.org/web/20210408142532/https://sympa.inri...

May I suggest "chkn".

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

Is anyone able to load the mailing list link at https://sympa.inria.fr/sympa/arc/coq-club/2021-04/msg00125.h... or is Sympa getting hugged to death? I'd like to read the discussion to understand more about the perspectives of people who feel uncomfortable with the name.

Yes, it did shut down. Other links related to it:

* wiki, where anyone can add proposals: https://github.com/coq/coq/wiki/Alternative-names

* chat: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneou...

* forum: https://coq.discourse.group/t/renaming-coq/1264

haha they can't get away from it https://github.com/coq/coq/wiki/Alternative-names#gaul

English speakers are quite selfish it seems. Instead of acknowledging and appreciating other languages they're tailoring those languages for themselves.

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.

This reminds me somewhat of the original name of JavaScript's Karma test runner: Testacular.

I didn't particularly mind the name, although it was kind of puerile. What I did increasingly mind is that every time I googled for it Google would come back with, "Did you mean testicular cancer?" (yes, really - this is not something I'd choose to joke about) and then show me results for that until I clicked through what it thought was the misspelled alternative.

That became rather tedious in fairly short order, and I suppose you could argue the name was in rather poor taste (though I was never particularly bothered), so I was immeasurably relieved when the team running the project chose to rename it to Karma.

I don't tend to get too bent out of shape about names in general since it's something of a programmer/engineer trope to occasionally use let's say more characterful names for projects and symbols and whilst there's a time and a place I'd hate to see it go away entirely.

what about the reverse problem? plain English words that mean something else in other languages. I am bit amused whenever an English speaking person shouts "Cut Cut Cut!" (I speak Dutch)

IBM introduced the RS/6000 "workstation" computer.

We got a memo that said not to use 'RS' in the name.

Apparently in the U.S. the use of 'BS' for Bullshit has Australian equivalent of 'RS' for Ratshit. Thus, the RatShit/6000 was born.

I found it funny but apparently the Marketing people didn't.

Hey Thierry Coquand please change your last name, it's offensive for me to write it down in this comment.

I like the suggestion "Capon": a neutered rooster

In English, a "cock" is also a name for a male chicken (a rooster). There's nothing wrong with "Coq". It was a good name and a good logo. Sorry it's changing.

I teach maths and English in the Danish public school to 14/15 year olds. The English word "pig" sounds a lot like "pik" (dick/dong/prick,etc) to Danish ears. I get to emphasise the distinction between hard-g and k, and the kids have a giggle at my expense. So what? I wish these puritanical idiots trying to control language and thought could get over themselves.

I am very happy to be living in a country which is not yet thoroughly infected by the PC poison seeping out of the anglosphere.

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.

I can only hope they end up with "hors coq".

Let's also change all conference names that end in "con" to something else. It is extremely offensive to french speakers.

People love renaming things and coming up with some reasoning why a name is offensive. A similar issue came up at one of the companies (in which I've worked) hack-a-thons, which is called Code Rage. A single person expressed how rage makes them think of road rage and not coding. Anyways their longer argument was that rage seems like a negative connotation. Even though rage probably refers to a "rager" or party, not aggressive driving.

There's another incident recently with a building proposal in NYC for a building called Penn 15. Because so many Americans still latch on to grade school humor, we can't get past the fact that if you remove an "n" it looks like Pen 15, or Penis if you squint and make enough puns.

They should rename the language to Cock, as in cocking a gun, cocking your head, or another name for a rooster. Grow the fuck up already.

Maybe the offending name as you personally initially interpreted, made you think it means something else. Perhaps you just need to seek more context around a name? Perhaps Coq needs to provide a more upfront representation and information of their chosen name?

I honestly don't disagree or agree and think we could all grow up a bit and have a more mature society if we didn't focus on petty insignificant changes to things like this.

Maybe we should all "grow the fuck up already", and it's likely that a majority of people have "grown the fuck up", but that doesn't really change anything. You can't just tell people to grow up and expect it to actually happen. The Penn 15 thing is a more ridiculous example, but if people are using the name "Coq" to make people uncomfortable, then that's just how it is, no amount of telling people to act like grownups is going to change that.

And even if it weren't making people uncomfortable, the fact is that it's harder to get management to sign off on using something like Coq if they feel it sounds like an "HR Violation Waiting to Happen". Changing to something more innocuous might work to get Coq used more in industry. As it stands, I almost never mention it at work anymore, and instead talk about TLAPS and Isabelle whenever I need to mention proof systems.

That's honestly too bad, I think telling people to grow does matter. It usually has to come from a respected person for it to latch on. I think worrying about every word being a potential "HR Violation Waiting to Happen" is an approach that leads to doubling down on these ideas as offensive, giving way to "only these words are appropriate" world.

I mean, part of me agrees with you, it's immature to make jokes about genitalia with an innocuous word in French and even if they did then a few stupid jokes isn't a big deal.

At the same time, I feel like it's really easy for me to say stuff like that, as a white male working in tech, a group that's never been unwelcome in STEM (at least not in my lifetime).

Absolutely fair and agreed.

My prof (who is French) once jokingly said this was a little prank by the French for the English speaking folks

In case anyone wants to check out their Wikipedia page: https://en.wikipedia.org/wiki/Coq

Translate and adapt it into Spanish.

"Polla".

It's just the national lottery in Chile.

What about cocktails? There are a lot of words in need for replacement. Do we need to replace Joe Cocker's grave. What about wankel engine, that sounds bad too.

We're on it. The world will be a better place afterwards.

the same people probably also find reading Kant offensive

Maybe just rebrand to be pronounced 'coke'?

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

Phallus?

Pretty sure that's how it's already supposed to be pronounced.

Reminds of Bro Lang changing to Zeek. Not clear on the reasons for the change but I think there’s some overlapping concerns

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.

Why not just make the logo an obvious rooster and lean into the jokes?

I’m rather surprised they don’t even have internal proposals.

They do, it's linked from the page: https://github.com/coq/coq/wiki/Alternative-names

Funny. Are they also going to rename Thierry Coquand?

Wow, I didn't even notice what it sounded like.

What about Le Coq Sportif? Will it also be renamed?

It's pretty obvious that "Le Coq Sportif" is part of a non-english brand name. Coq not so much, especially out of context - eg. people overhearing professional conversations about the theorem prover, or when trying to introduce it to new audiences. I'll accept it was a tit-for-tat joke back in the day (re. 'bit'), but the original namers should have foreseen this day coming. It's branding 101 to do your research and avoid these issues.

The hardest thing in Computer Science is naming things.

Roq sounds like a great name.

Is it correct to call the debate around renaming this a Coq-fight?

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?

So it seems like, but it has been ongoing for very long: https://www.youtube.com/watch?v=BM541-RBCwg&t=360s https://www.youtube.com/watch?v=z6tqt0aKCQo&t=18s

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.

That might be a regional difference: I've heard cock or cockerel plenty of times in British English. We even sang a song at primary school called "The Golden Cockerel" in assemblies: https://www.youtube.com/watch?v=IkoWrj_IBWo

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

It's a word that has, in the English language, been a euphemism for "penis" essentially forever.

https://www.etymonline.com/word/cock

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.

No longer will productivity be measured in "lines of coq." Pour one out.

> Le Coq Formel

I'm surprised this is a serious proposal. I can see everyone having fun with this at the project's expense.

The concern around women, NBs, and others being harassed for mentioning their work on the project is good feedback which I doubt many straight white men would've noticed or envisioned organically, so kudos to Wolf putting that concern front and center. It's a good reminder for why we should include diverse voices with us on a level decisioning/playing field.

Reply on news.ycombinator.com