Change of Name: Coq –> The Rocq Prover | Hacker News Reader

Change of Name: Coq –> The Rocq Prover

github.com

35 pointsluu48 comments

Reminds me of a time when i created a library to work with iterators in lisp, inadvertently naming it cl-iterators[0], as far as the naming convention of common lisp libraries went at that time. Some folks(including me!) on reddit had lots of fun with the unfortunate name.

[0] https://github.com/ykm/critter

I don’t have an opinion on the decision to change, but it’s a shame they switched to one so similar to https://www.roc-lang.org/

I assume avoiding confusion is part of the motivation for adding the stylised “q” at the end, but even so…

The discussions page notes the potential conflict:

Note: There exists an unreleased, under development programming language called Roc (named after the mythical bird) - https://roc-lang.org

What a sad day if it's acted, as a native french I always got a little chuckle that there is a slight comeuppance for the fact that 'bit' (and also 'byte' in a lesser measure) is pronounced exactly like 'bite', which is french for 'cock'.

It's harmless fun, and also a taste of the cultural hegemony the non-anglosaxon world get (I realize the irony of saying that as a french).

Anyway, I need to go to the store and ask the clerk for a 32 giga-cock USB drive.

Speaking of string (tong) was another funny thing in class when learning the craft.

I share your sadness, the difference in orthography makes it already very clear it's a different word.

For 'string', it's funny how desensitized you get the the word until you talk to a colleague and ask him "Mais du coup t'as un string ?", and realized you asked him in public if he had a tong.

Or when you try to debug something while a little tired, and mindlessly google 'string' without any other search term, only to be surprised at only having underwear-related results.

Weird, in french I always used feminine for character string ("T'as une string ?")

Yep, same: masculine for the underwear and feminine for the "chaine de caractères".

Source: https://fr.m.wiktionary.org/wiki/string

Well I didn't knew that, thanks for the info! It's a bit like "espace" which is feminine when talking about typography.

Or "covid", but only because I'm too stubborn to accept to say "La covid".

OK but definitely, always LE wifi. Not la wifi. Please. https://www.lawifi.fr/

I thought it would be une chaine but string, as franglais, would be le string ?

on the other hand, having misread your nick as « ma belle poule » I was inspired to google « belle poule » only to be surprised by a bunch of images of a sailing ship...

You should try to google "Poule Soie", they are gorgeous beast :)

The nickname is a play on my family name ("Monchablon"), that was wrongly written on the first draft of my work contract (as "Mablochon"), which only needed a bit of a chicken-obsessed CTO to become "Mablopoule".

One handy habit I got from that CTO is to keep a folder of images of poultry to use as test images when coding/debugging an image-related form.

Looks tempting: « La Poule Soie, avec sa silhouette toute ronde, est une excellent poule de compagnie. »

Unfortunately I imagine they're difficult to keep in urban environments; maybe some HN entrepreneurial type ought to start a "Chickens As A Service" site so those who don't have the facilities to keep poultry at home could rent them by the hour?

  *en frappant à la porte d'une fête à 3h00* 
  — « Bonsoir, c'est la police ; vos voisins nous ont appelés ... »
  — « Eh bien, allez à eux alors. Ici, on a commandé des poules, pas des flics »

I've had weird looks from people when I was talking about a dongle.

I meant the Logitech Unify one.

They were thinking of something else.

As an young anglophone enrolled in French immersion, I (nearly ~30 years later now) distinctly remember the day my teacher taught us about seals (phoques).

And yes, it's pronounced exactly like you think.

That was a glorious month or two until we moved on to the next module.

If I recall correctly, there is an etymological reason for this.

I seem to remember that the foc (it's a sail) is named after the phoque (the seal). And the foc is the sail that takes the wind from behind. I'll let you fill in the details.

Years ago I read somewhere a response by some of the Coq authors that, upon learning that some female students (outside of France) would get discouraged from working with the tool because the name had dirty connotations, they thought this was a naming mistake.

I’m pretty allergic to woke culture, and I still thought this is just better marketing.

People will keep calling it Coq, and newcomers will call it Rocq. There’s no deadnaming or stigma involved.

Seems Cockroach DB has proven more resilient to name shaming.

I love how the github is a wall of unrelated text to justify renaming away from Cock

I hope Thierry Rocquand gave his blessing

Kind of telling that they don't give a reason. Also "The Rocq Prover" is a terrible name. If you're going to go to the effort of renaming at least come up with a good one!

I wonder if anyone has tried to rename Git (roughly equivalent to 'asshole' in American).

The new name sounds related to AMD's ROCm.

It is worth reading the entire roadmap. These are all comprehensible and important points.

Coq seems to be a perpetual construction site.

Ltac -> Ltac2

Prop -> Sprop

On the other hand, my personal gimmicks a few years ago only touched on a tiny range of functions of the then Coq.

Therefore, I assume that most Coq users see more stability than you would think.

The page summarizing the considered new names and their pros/cons is interesting: https://github.com/coq/coq/wiki/Alternative-names

Naming is hard...

Why now? The innuendo has grown to be unbearable?

Americans.

English is not the only language.

America is not the only country, and theirs is not the only culture.

Problem solved by pronouncing it "cee-oh-queue".

The idiots won again.

Why?

傷害美國人民的感情

I dunno, your typical corporate employee is just copying the affectations of the upper class from thirty years ago, which was playacting you’re an incorporeal, sexless vessel for shareholder value while seeing a therapist. The trendsetters have moved on. In thirty years you’ll be taking ketamine and contributing to each other’s limited-run offline-only print magazines, since that’s what’s cool now.

Should rename it to Poissy

> 069-coq-roadmap.md

Nice

Fantastic news! Great to see that they've finally decided on a new and better name which the project most certainly deserves.

Great project; as to how they name it: « je m'en fous ».

Cool, now I can recommend it to female devs to learn, without anyone getting uncomfortable.

With the growth of lean, I suppose its time to get more serious in popularizing and attracting community instead of trying to pursue harmless chuckles.

Edit:

And I immediately get labeled as a "tranny protector". I'm not from the western world and we do not have the same cultural issues.

What I meant is, in a world where English nevertheless dominates as a common language by far, perhaps naming matters in the English context much more than any other language, particularly when building something for everyone.

Edit Edit:

I mean I had no idea there were such strong feelings of what i suppose is being perceived as American/English cultural interference that's felt so strongly by the French.

Maybe that's what Africans feel who were colonised by French Coqs (national animal)?

I now completely agree it is a brilliant idea to name something "cunt" in honour of Louvre Cuntadoodleur. :D

Anyone who was put off learning Coq by the name probably isn't the kind of person who'd grok or enjoy something as abstract and tedious as formal theorem proving.

Thank you for protecting women from the dangers of the French language.

They should change it to a nicer word, like 'bonheur' (pronounced 'boner'), which is french for happiness :)

Famous story involving Yvonne de Gaulle and the Queen of England.

The Queen asked what Mrs. de Gaulle desired the most now that she is retired, to which she replied (with a heavy French accent), "a penis".

The audience was mortified until the Queen herself realized the mistake and corrected her, "oh, happiness".

Then perhaps we ought to change the name for "bits" so that software making can be recommended to French women, without them feeling uncomfortable?

I don't disagree with the name change, but I do think it's quite a sad remark on the climate we find ourselves in that the female devs on your team might maybe possibly potentially find it uncomfortable, and that we even need to cater to that. I mean, it's not even an English name.

Bash seems like a better target given something like a billion women have been the recipients of physical violence globally. But what do I know. I’m not on the language police.

It's named after its creator, Thierry Coquand. It also happens to be the name of the national animal of France.

But I'm glad you can now recommend it to damsels in distress who would have been offended.

It's just not that hard. "Ah, if you're interested in formal methods, you might look into a language called Coq, that's c-o-q (named for one of its authors, a Frenchman)...".

No need to voluntarily dance around twisting our own shirts into knots for the bureau of thoughtcrime. People are reasonable, don't go out of your way to be an undesirable prick and you won't get in trouble.

All this masculine pearl clutching makes my eyes roll back in my head so far they're going to get stuck one of these days. "How do I safely manage my female reports?!?!" and related whingeing. Treat them like humans, don't hit on them, and sure as shit don't share details about your life in their 1:1's, it's your boss' responsibility to fake that interest, not your subordinates ffs.

Reply on news.ycombinator.com