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.
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.
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...
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.
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:
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.
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".
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.
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.
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.
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.
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.
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.
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).
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 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.
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.
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.
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?
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?
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.
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.
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...
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.
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.