Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Coq theorem prover is now called Rocq

rocq-prover.org

Post reply on HN
Print view View original

11–20 of 29 posts

Re: Coq theorem prover is now called Rocq

#11

Post by hansvm »

miningape wrote: post #6

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"

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.

Re: Coq theorem prover is now called Rocq

#14

Post by tptacek »

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.

Re: Coq theorem prover is now called Rocq

#16

Post by p-e-w »

fargle wrote: post #10

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

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.

Re: Coq theorem prover is now called Rocq

#18

Post by sillysaurusx »

tptacek wrote: post #14

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 embarras…

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.

Post reply on HN