Hacker News Reader

HNHacker News

Top New Best Ask Show Jobs

Comment by yodsanklai | Hacker News Reader

Full thread

yodsanklai·

I learned recently that the Coq project was renamed Rocq https://rocq-prover.org.

View on HN

Not even a wink or a nudge about why they renamed: https://rocq-prover.org/about#Name

The linked discussion is upfront about the name change, if it wasn't already obvious.

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

Ah, the community voted on it. The reason why the survey was proposed shall, however, remain a mystery.

I was not part of the survey but count me as someone who felt concern whenever I had to say it in a public or professional setting.

> how different Coq users use Coq differently and express different needs

> applying Coq to do software verification

> encourage others to learn and use Coq

To be clear, some people giggle when they read or hear the above and this is the reason.

According to the post, 24% "expressed discomfort: (it is uncomfortable or awkward to have to use the name Coq)"

PS: i am impressed by the time and effort that was given here to create fancy graphs, regressions, tests, etc...

Speaking of https://www.why3.org/

For completeness https://github.com/creusot-rs/creusot

The French were right about so many things.

Probably the right move.

Definitely not the right move. The old name was perfectly fine and allowed for harmless fun. They can obviously do what they wish, but IMO there's no good reason to destroy good clean fun just because it might upset the occasional person.

The developers of a serious academic tool may not have wanted their image to be "harmless fun," especially of a sort that can reasonably offend people and make it hard to talk about in formal settings. "Let's try [something that sounds like rock]" is going to be an easier sell to your boss than "Let's try [something that sounds like cock]."

Reply on news.ycombinator.com