Coq theorem prover is now called Rocq (rocq-prover.org)

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

[flagged]

Calling it rocq makes it seem harder.

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

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"

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

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

(2022) Previous discussions

(35 points, 47 comments) https://news.ycombinator.com/item?id=38779480

(61 points, 64 comments) https://news.ycombinator.com/item?id=41180007

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

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

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.

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

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

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