3 ms·

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

by yodsanklai 2y ago

rafram 2y ago
Probably the right move.
- bigstrat2003 2y ago
  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.
  - rafram 2y ago
    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]."
lelandfe 2y ago
Not even a wink or a nudge about why they renamed: https://rocq-prover.org/about#Name https://rocq-prover.org/about#Name
- SubjectToChange 2y ago
  The linked discussion is upfront about the name change, if it wasn't already obvious. https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001 https://coq.discourse.group/t/coq-community-survey-2022-resu...
  - lelandfe 2y ago
    Ah, the community voted on it. The reason why the survey was proposed shall, however, remain a mystery.
    - jghn 2y ago
      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.
    - thih9 2y ago
      > 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.
    - tacker2000 2y ago
      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...
- sitkack 2y ago
  Speaking of https://www.why3.org/ https://www.why3.org/ For completeness https://github.com/creusot-rs/creusot https://github.com/creusot-rs/creusot The French were right about so many things.

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

rafram 2y ago

Probably the right move.

bigstrat2003 2y ago
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.
- rafram 2y ago
  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]."

lelandfe 2y ago

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

SubjectToChange 2y ago
The linked discussion is upfront about the name change, if it wasn't already obvious. https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001 https://coq.discourse.group/t/coq-community-survey-2022-resu...
- lelandfe 2y ago
  Ah, the community voted on it. The reason why the survey was proposed shall, however, remain a mystery.
  - jghn 2y ago
    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.
  - thih9 2y ago
    > 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.
  - tacker2000 2y ago
    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...
sitkack 2y ago
Speaking of https://www.why3.org/ https://www.why3.org/ For completeness https://github.com/creusot-rs/creusot https://github.com/creusot-rs/creusot The French were right about so many things.