TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

Coq will be renamed into 'The Rocq Prover'

61 pointsby mvelbaum9 months ago

12 comments

dgacmu9 months ago
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.
评论 #41180956 未加载
评论 #41181047 未加载
评论 #41181138 未加载
评论 #41185705 未加载
评论 #41181085 未加载
michaelt9 months ago
Expanded details at <a href="https:&#x2F;&#x2F;coq.discourse.group&#x2F;t&#x2F;coq-community-survey-2022-results-part-iv-and-itp-paper-announcement&#x2F;2001" rel="nofollow">https:&#x2F;&#x2F;coq.discourse.group&#x2F;t&#x2F;coq-community-survey-2022-resu...</a><p>I&#x27;m not part of the Coq community so I&#x27;ve got no strong opinions on this. But I do know I&#x27;ve often heard people saying GIMP could do with a better name.
评论 #41180741 未加载
评论 #41185594 未加载
评论 #41180755 未加载
mauricioc9 months ago
Previously: <a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=38779480">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=38779480</a>
Cu3PO429 months ago
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:<p>&gt; No option receives more likes than dislikes.<p>So the new name was just &quot;the least bad&quot; 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.
评论 #41181022 未加载
aeonik9 months ago
I pronounce &quot;Coq&quot; with back of my throat to make it a bit different from the word &quot;Cock&quot;. Try to emulate the French accent a bit, and it ends of sounding almost like &quot;Coke&quot;, but not quite.<p>That being said context matters too, I still refer to loading a round into a gun&#x27;s chamber as cocking a gun.<p>I&#x27;ve never had an issue referencing the project&#x27;s name in a professional environment, where most of my colleagues are unfamiliar with it.
评论 #41181824 未加载
评论 #41182271 未加载
kerkeslager9 months ago
This isn&#x27;t a hill I&#x27;m willing to die on, but it&#x27;s mildly annoying that people couldn&#x27;t just grow up about this.
评论 #41181017 未加载
评论 #41181019 未加载
评论 #41181162 未加载
评论 #41180994 未加载
csneeky9 months ago
And what of the rooster mascot?
评论 #41180970 未加载
neilv9 months ago
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<p>We all appreciate various kinds of humor, in the right contexts.<p>But this software seems like something used in professional and academic contexts.<p>Including professional and academic contexts with a history of sometimes being unwelcoming to women. Who might not want to be reminded of old boys&#x27; club locker room phallic humor insensitivity throughout each day as they work.<p>So, the new name is going to seem like doubling-down, by those who didn&#x27;t understand all the problems with the previous name, or didn&#x27;t consider them problems.<p>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.<p>Now&#x27;s a chance avert some harm and regret.
评论 #41181336 未加载
djtango9 months ago
Rocq au vin
dist-epoch9 months ago
&gt; The Coq team has decided that Coq will be renamed into &#x27;The Rocq Prover&#x27;<p>They have a typo on the side, it&#x27;s `The Rocq Hard Prover`
sva_9 months ago
Sounds like an AMD product.
aestetix9 months ago
I can&#x27;t wait for someone to find a problem with this new name, and throw the entire project into disarray for another few years.