4 ms·

Coq theorem prover is now called Rocq

22 points by rwmj 6mo ago

nz 6mo ago
It's good to see that they have chosen a name that has a much more obvious and less confusing spelling.
yodon 6mo ago
[flagged]
booleandilemma 6mo ago
Calling it rocq makes it seem harder.
wk_end 6mo ago
They made this change a couple of years back, didn’t they?
miningape 6mo ago
I prefer the old name, it was much more memorable because it's funny. "Yeah I'm playing with my Coq to try and get it working again"
- hansvm 6mo ago
  standup> My coq experiments are promising, but it feels a little harder than it should be, and I'm worried it'll be too slow to deliver without some training and long practice sessions.
mcluck 6mo ago
Thank goodness. It's been impossible to talk about Coq to people who don't already know what it is.
mcdonje 6mo ago
While some may lament the departure of the phallus bird, nobody can be sad about the arrival of the giant fierce mythical bird.
gnabgib 6mo ago
(2022) Previous discussions (35 points, 47 comments) https://news.ycombinator.com/item?id=38779480 https://news.ycombinator.com/item?id=38779480 (61 points, 64 comments) https://news.ycombinator.com/item?id=41180007 https://news.ycombinator.com/item?id=41180007
fargle 6mo ago
why did they find the need to rename this? Am i missing something?
- LandR 6mo ago
  The name sounded like Cock.
- sillysaurusx 6mo ago
  [flagged]
- p-e-w 6mo ago
  Because U.S. English is everything, and people want it that way, and any concern about cultural imperialism that would immediately be brought up in any other context magically doesn’t apply when Americans could possibly be offended. Everyone else has to adapt, no matter their mother tongue. Meanwhile the world’s most common VCS’s name is literally an abuse (not a misspelling of one), but only outside the US so nobody cares.
  - llbbdd 6mo ago
    Practically speaking there's no reason not to centralize on the particulars of one language while the rest are in the increasingly accelerated process of dying out. Language barriers help nobody. Though it is a shame to rename this, the world needs more whimsy and penises are funny.
- deleted 6mo ago
  [deleted]
- tom_ 6mo ago
  The linked community survey suggests that a plurality of votes were in favour, which would explain it: https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001 https://discourse.rocq-prover.org/t/coq-community-survey-202...
fooker 6mo ago
Just in time for LEAN to have made it almost completely obsolete.
tptacek 6mo ago
The notoriety of Coq's name is, by a long, long way, the most embarrassing message board trope on HN. For years, you couldn't run a story about Coq --- a genuinely interesting and important piece of software --- on the front page without attracting sophomoric comments about a (bad) English transliteration? is that the word? of the name. So like 4 years ago they renamed it, literally for this reason, which is embarrassing all on its own, and that's still not enough to get HN to stop talking about it. I rarely do this, because the moderators really don't want anybody doing it, but I'll say out loud this time: I flagged this post. Just leave them alone.
- sillysaurusx 6mo ago
  Party pooper. We have so few opportunities to be silly on HN. Plus it’s good advertisement for what would otherwise be an obscure piece of software. You can’t deny it would be much less known. I’m not saying it was a good idea, just an oddity. There was no need to curb stomp it with a public declaration of nuisance. Oh well. Hey, thanks for the whiskey slap. I still think about it fondly.
- smnrchrds 6mo ago
  As a non-anglophone myself, I hate the fact that we have given one language so much power to dictate how every other country and language should name things. You will never find an American company changing the name of their product in the US because it sounds naughty in French. Yet here we are, a group of francophones feeling pressure to change their product's name for anglophones' sake.
  - adw 6mo ago
    The author knew fine that it was a knob joke (https://news.ycombinator.com/item?id=26743882 https://news.ycombinator.com/item?id=26743882). In this specific case, play stupid games, get stupid prizes; no-one is asking Le Coq Sportif to rebrand or your local bistro to stop serving coq au vin.
    - bestouff 6mo ago
ahartmetz 6mo ago
It used to be that you could write Coq in Kant (KDE's Kate editor before it was renamed for... similar reasons - though much much earlier / quicker).
andreweggleston 6mo ago
And now instead of being confused for a bad word, it gets confused with https://www.roc-lang.org/ https://www.roc-lang.org/
pjdkoch 6mo ago
That's gonna be easy to confuse with Roc, no?

22 points by rwmj 6mo ago

nz 6mo ago

It's good to see that they have chosen a name that has a much more obvious and less confusing spelling.

yodon 6mo ago

[flagged]

booleandilemma 6mo ago

Calling it rocq makes it seem harder.

wk_end 6mo ago

They made this change a couple of years back, didn’t they?

miningape 6mo ago

I prefer the old name, it was much more memorable because it's funny. "Yeah I'm playing with my Coq to try and get it working again"

hansvm 6mo ago
standup> My coq experiments are promising, but it feels a little harder than it should be, and I'm worried it'll be too slow to deliver without some training and long practice sessions.

mcluck 6mo ago

Thank goodness. It's been impossible to talk about Coq to people who don't already know what it is.

mcdonje 6mo ago

While some may lament the departure of the phallus bird, nobody can be sad about the arrival of the giant fierce mythical bird.

gnabgib 6mo ago

(2022) Previous discussions (35 points, 47 comments) https://news.ycombinator.com/item?id=38779480 https://news.ycombinator.com/item?id=38779480 (61 points, 64 comments) https://news.ycombinator.com/item?id=41180007 https://news.ycombinator.com/item?id=41180007

fargle 6mo ago

why did they find the need to rename this? Am i missing something?

LandR 6mo ago
The name sounded like Cock.
sillysaurusx 6mo ago
[flagged]
p-e-w 6mo ago
Because U.S. English is everything, and people want it that way, and any concern about cultural imperialism that would immediately be brought up in any other context magically doesn’t apply when Americans could possibly be offended. Everyone else has to adapt, no matter their mother tongue. Meanwhile the world’s most common VCS’s name is literally an abuse (not a misspelling of one), but only outside the US so nobody cares.
- llbbdd 6mo ago
  Practically speaking there's no reason not to centralize on the particulars of one language while the rest are in the increasingly accelerated process of dying out. Language barriers help nobody. Though it is a shame to rename this, the world needs more whimsy and penises are funny.
deleted 6mo ago
[deleted]
tom_ 6mo ago
The linked community survey suggests that a plurality of votes were in favour, which would explain it: https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001 https://discourse.rocq-prover.org/t/coq-community-survey-202...

fooker 6mo ago

Just in time for LEAN to have made it almost completely obsolete.

tptacek 6mo ago

The notoriety of Coq's name is, by a long, long way, the most embarrassing message board trope on HN. For years, you couldn't run a story about Coq --- a genuinely interesting and important piece of software --- on the front page without attracting sophomoric comments about a (bad) English transliteration? is that the word? of the name. So like 4 years ago they renamed it, literally for this reason, which is embarrassing all on its own, and that's still not enough to get HN to stop talking about it. I rarely do this, because the moderators really don't want anybody doing it, but I'll say out loud this time: I flagged this post. Just leave them alone.

sillysaurusx 6mo ago
Party pooper. We have so few opportunities to be silly on HN. Plus it’s good advertisement for what would otherwise be an obscure piece of software. You can’t deny it would be much less known. I’m not saying it was a good idea, just an oddity. There was no need to curb stomp it with a public declaration of nuisance. Oh well. Hey, thanks for the whiskey slap. I still think about it fondly.
smnrchrds 6mo ago
As a non-anglophone myself, I hate the fact that we have given one language so much power to dictate how every other country and language should name things. You will never find an American company changing the name of their product in the US because it sounds naughty in French. Yet here we are, a group of francophones feeling pressure to change their product's name for anglophones' sake.
- adw 6mo ago
  The author knew fine that it was a knob joke (https://news.ycombinator.com/item?id=26743882 https://news.ycombinator.com/item?id=26743882). In this specific case, play stupid games, get stupid prizes; no-one is asking Le Coq Sportif to rebrand or your local bistro to stop serving coq au vin.
  - bestouff 6mo ago

ahartmetz 6mo ago

It used to be that you could write Coq in Kant (KDE's Kate editor before it was renamed for... similar reasons - though much much earlier / quicker).

andreweggleston 6mo ago

And now instead of being confused for a bad word, it gets confused with https://www.roc-lang.org/ https://www.roc-lang.org/

pjdkoch 6mo ago

That's gonna be easy to confuse with Roc, no?