Coq will be renamed into 'The Rocq Prover' | Hacker News Reader

Coq will be renamed into 'The Rocq Prover'

coq.inria.fr

61 pointsmvelbaum64 comments

I will say that as a professor who occasionally has to refer to this system in front of a bunch of (American) 18-24 year olds, I'm very grateful for this renaming.

As a recent graduate I'll miss asking for "help with my Coq" and proclaiming "my Coq isn't working" during lab sessions

So that's why I never hear any students complaining about how hard it is

As a native french speaker I am quite surprised by those reactions. 'Bit', means 'dick'/'cock' in french, and it's never really been a big issue at university.

Bit sounds so romantic in French.

Don't forget strings, that are sexy underwear....

And mac that means pimp ^^

I wonder if it's more due to the strength of sexual taboos in America or the frequency of the word -- bits are referred to from the very beginning of the curriculum, whereas theorem provers are only mentioned a few times unless you take a specific class. Both, perhaps - we are still a bit puritanical.

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

Coq blocked again!

Be honest, do you genuinely think people who would have giggled about this aren't going to keep using the old name pruriently?

Oh, I don't care what people say, I just find it distracting when I say the name in class, and there's a wave of "uh, what did he just say?" that percolates through the students.

"The French love the Coq". https://www.youtube.com/watch?v=_7plURl4sx4

(This guy is now one of our deputy prime ministers, le sigh)

Expanded details at https://coq.discourse.group/t/coq-community-survey-2022-resu...

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.

git has always been funny to me — as a Brit, at least. GitHub even more so.

git was intentionally given its name by Linus is the joke.

Everyone else bandwagoning onto it is the lol.

Yes! So I’ve read. But since he’s not British I’ve always wondered whether he completely understood the feel of the the word and quite how weird it sounds (to those not already used to it).

Maybe from Monty Python. Programmers love python.

Why wouldn't he? It's not like British culture is totally impenetrable. Any European over 35 will have ingested a lot of British television reruns over the course of the eighties and nineties. While that won't allow for every nuance, the word 'git' certainly is used in its proper context often enough.

Well, no culture is totally impenetrable with enough exposure/effort. I just wondered how much exposure he had. His English is obviously (beyond) native level but I do feel the subtlety of British English expressions are frequently lost. [*] Europeans, despite their relative geographic and cultural proximity, rarely seem to get British humour and expressions. American culture dominates these days anyway, no matter what you learnt in school.

For example, I wonder if he would have thought it was too far to call it ‘prick’?

Knowing Linus, perhaps not!

[*] (Not because there’s more subtlety than in any other culture/language; all locales have their own unique usages that are hard to truly understand unless you’ve lived there. I’m not claiming there’s anything mythical or unique about BE.)

As a non Brit, what is the feel of the word? Is it like having a site named IdiotHub?

More like AssholeHub. But not so rude.

They're exaggerating. It's a very casual insult, often used playfully

I thought so when I was younger, but I’ve found that it’s often considered worse than words like ‘idiot’ or ‘twit’. Some seem to find it — to my surprise — not just insulting, but crude.

In the 00s there was a popular wine called "old git". It generally means someone grumpy and cantankerous, but in a playful way (otherwise you'd just call them a c***). So it makes sense for a self-effacing joke about Linus Torvalds.

This is true. But I think there’s a surprising difference between calling someone ‘an old git’ / ‘a jammy git’ / ‘a grumpy git’ / … and simply calling them ‘a git’. The latter seems quite a lot harsher and less likely to be a joke.

He's Finnish. Most of the English-second-language speaking world learns British English, so I'd expect that he definitely understood the word.

> I'm an egotistical bastard, and I name all my projects after myself. First 'Linux', now 'Git'".

It seems he knew, but I can say I never learned "git" in school.

>British English

Academia it's just a few years long. After that... the 90% of the media it's American English.

I haven’t met many Finns, but the Swedes I’ve met seem to have learnt most of their English from watching American television and YouTubers. Knowing a word isn’t the same as having a lifetime of hearing it in varying contexts.

It's reasonable to assume that he knew the Monty Python reference.

https://www.youtube.com/watch?v=uLlv_aZjHXc&t=70s

I just noticed that the man page for git calls it "git - the stupid content tracker"

> Change the pronunciation to C.O.Q.

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

4 years ago gimp was forked into glimpse. It is a hugely popular fork. You can't even see it's github because of the huge amount of commits.

Previously: https://news.ycombinator.com/item?id=38779480

I have no strong opinion on renaming the project as such and conducting a survey was surely one of the better ways to handle that question. However, one thing in their evaluation of alternative names sprung out at me:

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

Did the options include "don't change it" and did that perform worse than any given new name?

It doesn’t seem so, but by a slight majority on overall respondents it seems like changing the name was favored.

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

Whether the name should be changed was a separate question and there was a slight majority in favor of changing it. Among respondents who favored changing the name, there were options that were more liked than disliked, but not by the entire community.

You really should take a look at their evaluation. It's quite comprehensive: https://coq.discourse.group/t/coq-community-survey-2022-resu...

I pronounce "Coq" with back of my throat to make it a bit different from the word "Cock". Try to emulate the French accent a bit, and it ends of sounding almost like "Coke", but not quite.

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.

If you're willing to put a bit of time in phonology, English initial c/k is always aspirated (i.e. pronounced with a significant and sudden exhalation) and French initial hard c/k is always unaspirated. The one thing that can have you emulate the French pronunciation the most is by learning to pronounce initial k/t/p in an unaspirated way.

> That being said context matters too, I still refer to loading a round into a gun's chamber as cocking a gun.

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.

This isn't a hill I'm willing to die on, but it's mildly annoying that people couldn't just grow up about this.

Isn’t it supposed to be pronounced more like “coke” anyhow?

No not the French word or name, and neither is the German word "Koch" for that matter.

There's no real English way to pronounce it properly without doing it the French way: https://www.google.com/search?q=coq+french+pronouce

Specific cohorts do grow up, but also new generations enter college every year. :)

And some people really never do grow up in this topic's sense, even in non-native English speaking countries.

totally agree. I mean it's not like "cock" isn't a totally normal word for a male chicken. I bet biology students or ornithologists are the only ones who have grown up in that regard...

And what of the rooster mascot?

The new mascot will be a phallos.

Someone on HN pointed out a problem with a joke in the new name, but they got flagged. Basically, the new name looks like intentional innuendo wordplay related to the problem with the first name

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.

> Basically, the new name looks like intentional innuendo wordplay related to the problem with the first name

Maybe I'm stupid (or my English isn't good enough), but I don't see the innuendo.

I also am unable to see what the new innuendo is

If they go through with the name, it'll be pointed out and well known, and then people will realize "oh, that's the intended joke...".

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.

I'm honestly guessing here because I'm not an insider and I don't naturally understand what's going on with this made up word, but I think it's:

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

Rocq au vin

> The Coq team has decided that Coq will be renamed into 'The Rocq Prover'

They have a typo on the side, it's `The Rocq Hard Prover`

Sounds like an AMD product.

I can't wait for someone to find a problem with this new name, and throw the entire project into disarray for another few years.

Reply on news.ycombinator.com