from Hacker News

Coq will be renamed into 'The Rocq Prover'

by mvelbaum on 8/7/24, 10:47 AM with 64 comments

  • by dgacmu on 8/7/24, 12:44 PM

    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.

  • by michaelt on 8/7/24, 12:28 PM

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

    I'm not part of the Coq community so I've got no strong opinions on this. But I do know I've often heard people saying GIMP could do with a better name.

  • by mauricioc on 8/7/24, 12:37 PM

  • by Cu3PO42 on 8/7/24, 12:39 PM

    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:

    > No option receives more likes than dislikes.

    So the new name was just "the least bad" 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.

  • by aeonik on 8/7/24, 1:59 PM

    I pronounce "Coq" with back of my throat to make it a bit different from the word "Cock". Try to emulate the French accent a bit, and it ends of sounding almost like "Coke", but not quite.

    That being said context matters too, I still refer to loading a round into a gun's chamber as cocking a gun.

    I've never had an issue referencing the project's name in a professional environment, where most of my colleagues are unfamiliar with it.

  • by kerkeslager on 8/7/24, 12:49 PM

    This isn't a hill I'm willing to die on, but it's mildly annoying that people couldn't just grow up about this.

  • by csneeky on 8/7/24, 12:55 PM

    And what of the rooster mascot?

  • by neilv on 8/7/24, 1:19 PM

    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

    We all appreciate various kinds of humor, in the right contexts.

    But this software seems like something used in professional and academic contexts.

    Including professional and academic contexts with a history of sometimes being unwelcoming to women. Who might not want to be reminded of old boys' club locker room phallic humor insensitivity throughout each day as they work.

    So, the new name is going to seem like doubling-down, by those who didn't understand all the problems with the previous name, or didn't consider them problems.

    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.

    Now's a chance avert some harm and regret.

  • by djtango on 8/7/24, 12:43 PM

    Rocq au vin

  • by dist-epoch on 8/7/24, 1:23 PM

    > The Coq team has decided that Coq will be renamed into 'The Rocq Prover'

    They have a typo on the side, it's `The Rocq Hard Prover`

  • by sva_ on 8/7/24, 12:45 PM

    Sounds like an AMD product.

  • by aestetix on 8/7/24, 1:02 PM

    I can't wait for someone to find a problem with this new name, and throw the entire project into disarray for another few years.