I don't think this has anything to do with "American puritanism" or 21st century something. Giving a project a name that sound exactly like "cock" is just plain bad.

Imagine for a second that your favourite programming language or the one you use at work was called "Penis"? How would that change the perceived seriousness of the language? How fun would it be when you told someone "we use Penis where I work to implement our AwesomeSoftware™?

I use Coq on a daily bases and I've gotten many funny looks when talking about "cock" to people who are not familiar with it. It doesn't bother me much but there is nothing _positive_ about a name like that.

> Imagine for a second that your favourite programming language or the one you use at work was called "Penis"

No need to imagine, "bit" is pronounced in French exactly like "bite", which means basically the same thing as "cock".

> How fun would it be when you told someone "we use Penis where I work to implement our AwesomeSoftware™?

You get used to it. Talking about "cock twiddling" sounds strange at first, and is annoying. But since we're French we can't really hope that this will change anytime soon.

Anyways, I'm all for changing the name, but hope we can keep the French origin. "LPC" for "Le Prouveur Coq" is a good idea https://github.com/coq/coq/wiki/Alternative-names.

It is not an ideal name, I agree. On the other hand, it is the french word for an animal, and not for the male genital organs.

What about the word bite (la bite) in french? Are we supposed to remove the word bit from the English language because it sounds similar to the french word for penis?

There is always going to be strange overlaps when it comes to different languages.

No, but you might want to take it into acccount if you're naming a software project lots of French-speakers will be involved with.

French have more humor when it comes to sexual references, it wouldn't surprise me if a name like that would actually be an asset. (Source: myself, French, living abroad).

Only if it makes sense for the product to make a sexual reference. (Source: myself, French, living abroad, worked in marketing/branding).

Coq is a bad name.

Or you know, Americans can learn that the world is not theirs, and they have no command or say over foreign words, just because they resemble phonetically (!!!) some word they consider shameful and sinful!

I'm confused why you think Americans are relevant to this story. The word "cock" and it's status as an English language vulgarity is a product of England. It predates the U.S. by centuries.

Because in 2021, the British are mature enough not to care.

It's those that inherited the culture of the puritans they've sent away that make a fuss about it (or some words on tv or make a huge deal about a SuperBowl nip slip).

Sure, but that doesn't really change anything about the fact that when an American hears "Coq" they also hear "cock."

There are many similar stories about English words sounding like profanity when (badly) pronounced in Chinese.

They're bad for branding and brands avoid them.

Now, I like "Coq" and the story about the cheeky French people trying to one up anglophones, but that's not really enough to make it a good name.

Then again I recall some people calling a compiler "Stalin" so, could be worse.

> Imagine for a second that your favourite programming language or the one you use at work was called "Penis"?

Except "penis" isn't ambiguous. Coq is French for cock -- as in rooster. If you have an issue with the name Coq, chances are you're too infantile to make meaningful use of it or contribute anything of value to it whatsoever.

In English. You forgot to point out that you comment was from a rabidly anglocentric point of view. There are, in fact, lots of other languages. Furthermore we like one- and two-syllable names for our programming languages. Being a quantitatively-minded person you will appreciate that this implies that it is likely that e.g. ruby means something rude in swahili or whatever.

The whole computer science/programming field is anglocentric and the problem with Coq doesn't occur just in english speaking countries. English is not my primary language, but since the sound "coq" doesn't mean anything in my primary language, and since everybody in my country speak english as a secondary language, most people will still parse the sound "Coq" as "cock" and think of the non-ideal english meaning of that.

A name accidentally meaning something bad in one language is a lot worse than a name intentionally meaning something bad in a language that 100% of its userbase speaks and understands.

>I don't think this has anything to do with "American puritanism" or 21st century something. Giving a project a name that sound exactly like "cock" is just plain bad.

You do know that coq is a perfectly fine french word, and also in the name of a big french sports brand, right?

Not to mention that "cock" is mere slang, the official word just means rooster.

Please don't use the word "pick". It sounds exactly like the Dutch word for penis.

Also don't use the word "could" because in Dutch that sounds like a nasty word for vagina.

Thanks for being considerate. There is nothing wrong with your English language, but sometimes it sounds offensive in mine.

Nah. I'm joking obviously. I do understand that in an international project with the dominance of English it makes it easier to take these things into account. I don't blame them for looking for a new name.

But the idea that the whole world changes their values and language constructs to not offend American sexual oppressive culture is still stupid. I do blame Americans for that.

> But the idea that the whole world changes their values and language constructs to not offend American sexual oppressive culture is still stupid.

I completely agree with that. If anyone demands that then that I would certainly not agree with that. But, I don't think that is what this is about at all. It's my impression that most people who think Coq should get a new name aren't "offended", they just think it's a bad name and that Coq should have a good name.

"Pick" actually sounds like penis in my native language (danish) as well, and I'm pretty sure that a danish company launching a product for the danish market would avoid the name "Pick". I assume that if you where to launch a product in the Netherlands you would avoid naming it "Pick" as well?

> I assume that if you where to launch a product in the Netherlands you would avoid naming it "Pick" as well?

Not really. But its not a fair comparision, because Coq isn't an American or British research project, its a french project. Its not even a commercial product or anything.

So i fully understand they want to change their name, but it is sad they feel forced to. Honestly, if someone is harressed by actual adults within a particular culture for using something that could somehow make a 14 year old little boy giggle, then i strongly suggest they leave whatever culture they are in, because its completely backwards.

The problem to infantile behavior and sexism in particular cultures isn't sovled by every other culture renaming their stuff to not trigger this behavior. Lets solve sexual harrassment in English speaking countries by the rest of the world avoiding doing anything that has any phonetic resembles to genitals. Does that not sound idiotic? Is that a not a weird English privilege that other languages don't get?

Again i understand and respect the decision by the project. In the end you just dont want people to get harressed. But lets not pretend the problem is the name. The problem is certain cultures lacking adult behavioral norms for men.

See also: Mövenpick the ice cream brand https://www.moevenpick-icecream.com/ where moven are birds

Well, Kavli (as in "Kavli Crispy Garlic" snack and the Kavli foundation) means "big cock" in Greek.

Would anyone be even remotely offended? No...

>How fun would it be when you told someone "we use Penis where I work to implement our AwesomeSoftware™?

It would be a non-issue for people beyond middle school?

And doubly so if the term was a regular foreign word.

Are people also taken aback when somebody asks for some coke with their food?

What prevents you and everyone else to just pronounce it as an acronym?

Whose fault is it they hear "cock" and they think of "penis"? We're not talking about GIMP here. It just means people have a dirty mind and don't know about the programming language.

Worse than a dirty mind: a mind that can't handle maturity.

I remember reading (and I don't have a source for this so this is total hearsay) that basically when Coq/CoC was chosen, it was chosen with the awareness of the "sounds like cock lol" factor being a plus.

This is far from the first "french mathematicians with a 10-year-old's sense of humor" thing, and probably won't be the last, but all this "oh it's just a word in French" is, from my undrestanding, bait.

To be honest, I'm not super convinced the process discussed the article is happening in much good faith either. But that's just my opinion and heavily biased towards my own experiences interacting with people from Inria.

That's what I thought at first, but apparently they were completely aware of the double meaning and gleeful about it.

In any case, it doesn't matter, because we don't need to keep having humiliating conversations about it, just change the damn name.

Of course they were aware of it. It requires not even basic proficiency of English. But at what point is it decided upon that the name was chosen just to rile people, and by whom? By you, depending on what mood you're in on the day in question? Humiliating conversations around these topics are only initiated by people like yourself when you decide to feel offended by harmless notions. The behavior shouldn't be dignified.

You are in fact the one choosing to be offended, and responding with personal attacks and vitriol. What's your problem with respecting women?

None. Neither the word coq (nor cock) is disrespecting of women any more than the word pussy is disrespecting of men. Get a grip of yourself and your moral panic.

Okay buddy, moral panic got it. Have a great career.

Why? To appease puritans? I‘d rather have them release a library for coq named tits (after the birds of course).

You can keep have genitalia discussions down at the pub, see how many women want to listen to you talk Coq.

We don't need Coq double entendres in the workplace, but we do need smart women in the theorem proving community.

(Potentially-relevant fact: I am a woman.)

I first heard of Coq in a CS lecture, and it wasn’t at all off-putting. The professor included the obligatory “yes the name sounds funny” disclaimer and then presented an interesting walkthrough of Coq. I haven’t used Coq myself yet, but that has more to do with the difficulty of starting than the name. I’ve enjoyed the Natural Number Game (a web-based set of Lean exercises), as a good example of something which actually helps people get into theorem proving. This debate over the name of Coq is just an instance of the Law of Triviality.

While you may not have felt that way, other women have. Does your experience invalidate theirs?

No, I’m just providing my own n=1.

(Why is it that “I am unhappy” is justified to report, but “I am alright” isn’t? Don’t we want a representative sample of opinions?)

It's perfectly fine, and in mature settings it should be a non-issue. But I've learnt to be wary of assuming everyone is fine with it, or assuming that everyone will behave. I mean, tech bros will tech bro. I'm not in favour of helping them perform deniable harassment.

This is harmless banter and anyone not resilient enough to handle this will face much greater distress during their working life. Adults should be able to handle childish humor and this movement towards infantilizing women seems a much greater issue to me. All this will achieve is giving power to political narcissist.

Interesting, how you’re so set on the name of a theorem proving software being the barrier to women entering the field and not the people who would actually harass them. Do you not think the same people who would make stupid jokes about a name wouldn’t find some other way to chase women away?

I'm just listening to what women say. You should try it sometime.

https://twitter.com/sydgibs/status/1379518799699968005

The name lends itself for innuendos, so what? I can assure you that a person with sleazy intentions will find many ways to do that without a funnily named programming language. The name is not the problem. Also, a person's offense is not an argument. I'm offended by your name, do you have to change it now? A funnily named programming language just isn't the same as actual sexual harassment.

Women are not children, they understand and appreciate humour. You being offended on behalf of them frankly seems more insulting. This kind of hyper-sensitive attitude is what drives women away from CS, not the word "coq".

Well, it's actually women in CS being offended, and I'm merely engaging with the blockheads who refuse to acknowledge the issue.

Are there real people offended by it? Or just three Twitter users?

Quite an accusation from a sockpuppet account that has been completely dormant since 2017.

Ah yes, sockpuppet. The term people use when they have good arguments.

Look at the account, it's a classic phony, stashed away for sniping without new account green.

Do you really think I played such a long game? In any case the other commenter is right -- you shouldn't attack the person, but the argument itself.

No smart theorem proving woman has ever been turned down by Coq. I know this because they would need to be familiar with Coq in the first place. Or would they have trained on Prolog instead?

Your statement doesn't follow any logic.

Tits alternative is a great theorem in mathematics.

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

I've had conversations with colleagues about the use of 'master' and 'slave' which appear to also be falling out of favour. Had mentioned that forking and killing children seems to be acceptable language, for now.

Perhaps I'll have to go back to school and re-learn English.

I still have an installation of GIMP.

I once worked at a campus disability resource center and was encouraging the use of open source software. It was not comfortable pitching the GIMP as a Photoshop alternative. Luckily I don't think anyone felt personally attacked and it was understood to be an unfortunate coincidence. One person said, "I guess that's what people call me." which brought to the fore how even coincidental naming issues can remind people of something unpleasant.

When it comes to Coq, I have a colleague that likes to emphasize the pun. It does turn some people off when they hear him going on about it. On the other hand, there is a lot of puritanical thinking in the US and maybe we should just become more comfortable with the notion that sexual organs, like mouths and elbows are part of the body. Then maybe my friend's "joke" wouldn't even make sense. It would be like "haha nose!" and people would shrug. But that isn't the world we live in and maybe the one we live in, where people find penises funny or offensive, is more fun. I don't know.

I'm not really advocating renaming stuff or not. I see it as more of a dialog between the namers and the people who are bothered, at least with borderline cases like these. There are instances where names should be changed. Like there are ISO-639 codes that essentially use the equivalent of the N-word to refer to languages. That's really hurtful to minority communities that speak those languages. Names do have consequences. I guess it is just a question of whether people are ok with the consequences or not. And of course, you can't make everyone happy all the time.

> you can't make everyone happy all the time.

Indeed.

I think when I'd heard of GIMP it maybe raised an eyebrow but nothing much beyond that. Anything more about it just seems like an immature and probably harmless joke, but that's just me.

When it comes to genitalia, there's literally hundreds of euphemisms - which seems to be the nature that language takes for primal things. There has to be a balance or Johnson & Johnson may need to rethink their name, too.

I remember being irritated as a kid from "master" and "slave" switches on ATA hard disks. I found it really weird that the serious hardware company chose such a colorful metaphor (I think I associated it more with certain sexual practices than historical slavery).

Now I'm used to the terms and don't make the connection anymore. They might as well be completely unrelated words written "mahsta" and "slehf" that just happen to sound like other bad words. In these and similar cases, I'd personally rather keep the innocent meaning of the words, and discourage the original meaning. "Slave" is just a device on I2C, why would you call a forced servant that? And why would you call somebody who committed the unthinkable crime of claiming to another human as "master"?

One very unfortunate name I'm surprized nobody has latched on to is MongoDB...

> Perhaps I'll have to go back to school and re-learn English.

Absurd hyperbole.

“ These days, these days, right, if you say you're English, you'll be arrested and thrown in jail!”

I wonder if they end up renaming git branches, because it's not very inclusive to ask certain coworkers what branch they are on

The main problem with GIMP's name is that it clashes with GIMPS - the Great Internet Mersenne Prime Search.

I thought forking referred to what's happening to the process tree, similar to what forking means in chess.

That's the entire point. Coq doesn't mean male genitalia either. But because it happens to spelled or sound like another word it is treated like that word.

English speakers who get offended by it can just spell "cee-oh-queue" and be done with it...

Indeed, a rebranding to that seems much saner. Perhaps they fear that such a change can't be forced upon the existing users, which is not an invalid concern either.

Wait till they learn what a Megabit means in French...

Today I learned that "bit" sounds to the French like "coq" sounds to the English.

Swapping bits. Doing arithmetic with bits. A nibble has not one but four bits. All fascinating stuff.

As someone who’s not a native English speaker and who doesn’t use Coq I feel I can’t even be bothered to take a stand in this question. Whatever. Hopefully the people in the community can do what they feel is good for current and future Coq users.

Has anyone informed the sports brand Le Coq Sportif of this? If you can have a 100million+ annual revenue with coq in your name, surely this namechange is beyond ridiculous?

Context is important.

It is, and Coq is a piece of software to prove theorems. The context in which it is used makes it trivially inoffensive.

Personally, I spent a semester trying Coq and I couldn't get used to it. My professor loved Coq, though. He was a mathematician, so it wasn't a huge surprise.

... yet they had a Dick Cheney as vice president

And the name was the least offensive part.

Here's hoping they reveal the new name and it's Weiner.

Did you mean Wiener?

No! Maybe. Argh.

This is reductive. Programming languages, for better or worse, are almost 100% in English. Having such a word as its name is not helpful to the project.

Except where they aren't.[1]

Mostly or overwhelmingly programming languages are written in English, but not 100%.

https://en.wikipedia.org/wiki/Non-English-based_programming_...

Did you miss the 'almost' in the comment you're replying to?

Heck, early version of basic for windows had translated function names. I dont know if MSFT is crazy enough to do that these days, but it was a major PITA and pretty hilarious back then.

They said “almost”.