After a lot of exposure, I map "coq" in a CS context to the theorem prover and don't find it giggle-worthy, but the reaction of students hearing it for the first time is different. (And outside of that, I'm more likely to think coq au vin, but I'm a cook.)
(This guy is now one of our deputy prime ministers, le sigh)
I'm not part of the Coq community so I've got no strong opinions on this. But I do know I've often heard people saying GIMP could do with a better name.
> People might not adopt it
Well, people were made to pronounce "CoC" as "C. O. C." or "code of conduct" instead of, you know, "Coq", and since Rocq community does have CoC, they could make people to adopt this pronunciation, absolutely.
> No option receives more likes than dislikes.
So the new name was just "the least bad" option. Naming things is hard and getting a community to agree on a name is surely that much harder still, but I still find it a bit sad that the new name is not well-liked.
You really should take a look at their evaluation. It's quite comprehensive: https://coq.discourse.group/t/coq-community-survey-2022-resu...
From the post it seems that anglophones were significantly (as in statistically) more likely to change the name for exactly the reason one can imagine
That being said context matters too, I still refer to loading a round into a gun's chamber as cocking a gun.
I've never had an issue referencing the project's name in a professional environment, where most of my colleagues are unfamiliar with it.
There are multiple meanings of the term, but depending on where you grow up, there may only be one in common use. When I grew up, there was only one meaning of the word, similar to ass, even though that had alternative meanings.
And some people really never do grow up in this topic's sense, even in non-native English speaking countries.
We all appreciate various kinds of humor, in the right contexts.
But this software seems like something used in professional and academic contexts.
Including professional and academic contexts with a history of sometimes being unwelcoming to women. Who might not want to be reminded of old boys' club locker room phallic humor insensitivity throughout each day as they work.
So, the new name is going to seem like doubling-down, by those who didn't understand all the problems with the previous name, or didn't consider them problems.
I think this is one of those things we sometimes do out of lighthearted intention, with no harm intended, and only later realize and regret.
Now's a chance avert some harm and regret.
Maybe I'm stupid (or my English isn't good enough), but I don't see the innuendo.
1. Name is "coq" which is pronounced like "cock". Tee hee hee I'm so funny I made you say a bad word. (Opinions can differ, but this word being bad isn't a terribly rare opinion IMO.)
2. Obviously, that means Q (at the end of a word!? *) is pronounced like a hard K.
3. Enough people don't like being "forced" to say that word, pick a new name, new name is "rocq". I was confused like you for a while until I figured out the above. If q->k, then this is pronounced "rock".
4. New name learner: Why in the world would you pronounce a Q (at the end of a word) as a K? (and/or) How am I supposed to pronounce that name? I've never seen a word like that before.
5. Oh, tee hee, because of an immature joke from the old name. (Have to explain the old name and make the innuendo, to make the new name make any sense. And the new name makes so little sense, it would be very natural to ask how it came about.)
* https://scrabblewordfinder.org/words-ending-in/q Which never happens -- have you heard of any of these words before? I haven't. (Besides I guess "tranq" which is really an abbreviation.)
Then they won't be able to type and say it during their workday, without at least silently cringing or smirking, at phallic humor being forced upon people in the workplace.
They have a typo on the side, it's `The Rocq Hard Prover`
