Yishuai Li (Apr 06 2021 at 14:07): Yishuai Li (Apr 06 2021 at 14:07):Consider changing "Coq Proof Assistant" into "L'Assistant de Preuve Coq" so that English speakers are liberated to interpret it in any way (e.g. "Rooster Proof Assistant")?
Context: https://sympa.inria.fr/sympa/arc/coq-club/2021-04/msg00006.html
Théo Zimmermann (Apr 06 2021 at 14:10):Hey! Is there any reason why you're making this suggestion on Zulip rather than in the ongoing Coq-Club discussion? The Zulip members who are not Coq-Club subscribers might be lacking context.
Yishuai Li (Apr 06 2021 at 14:13):I received a private email from James that he wanted to discuss logo change and I derailed his discussion.
Kenji Maillard (Apr 06 2021 at 14:26):Zulip is probably a better place to brainstorm without spamming the entire Coq world. Propositions/conclusions could be relayed afterward on the mailing list
Théo Zimmermann (Apr 06 2021 at 14:53):OK, then I'll add here that I feel like if people think that changing the way Coq is pronounced (rather than written) is the best solution, then I like the idea of pronouncing it co-Q better than the idea of spelling it out.
Pierre-Marie Pédrot (Apr 06 2021 at 14:56):it could even be read "ubiquinone" (https://en.wikipedia.org/wiki/Coenzyme_Q10)
Kenji Maillard (Apr 06 2021 at 14:58):Why "ubiquinone" rather than the fully reduced version "ubiquinol" ?
Pierre-Marie Pédrot (Apr 06 2021 at 15:04):Everybody knows that strongly normalizing your proof terms is a bad idea...
Yishuai Li (Apr 06 2021 at 15:07):My main concern is whether "kok" is a wrong pronunciation.
There is a list for learners of how terms should and should not be pronounced: https://github.com/shimohq/chinese-programmer-wrong-pronunciation
and I'm reluctant to put "kok" in the "wrong" column.
Pierre-Marie Pédrot (Apr 06 2021 at 15:08):For Chinese speakers, the important point is that the first consonant in "Coq" is not aspirated, contrarily to what English speakers pronounce.
Pierre-Marie Pédrot (Apr 06 2021 at 15:15):in IPA: English ['kʰɒk] vs. French ['kɔk] (although due to my Parisian accent, I personally slightly palatalize the coda)
Emilio Jesús Gallego Arias (Apr 06 2021 at 15:20):Gallina is pretty problematic in Spanish tho O_O
Yishuai Li (Apr 06 2021 at 15:24):@Pierre-Marie Pédrot Thanks for the instruction! I'll tell people to forget about the English pronunciation and approximate it by pinyin "gōqi".
Stefan Monnier (Apr 06 2021 at 15:28):It's actually a nice reversal of the joke, indeed, since when read in
French "co-Q" would be pronounced just like "cocu" (which means that
your spouse is cheating on you).
Théo Zimmermann (Apr 06 2021 at 15:29):Emilio Jesús Gallego Arias said:
Gallina is pretty problematic in Spanish tho O_O
:face_palm: looks like there isn't any perfect solution
Emilio Jesús Gallego Arias (Apr 06 2021 at 15:34):I was a bit kidding, but indeed Gallina in Spanish have some funny meanings, and say "I work on Gallina" sounds extremely weird and has undesired interpretations by farmers such as those from my place of origin; but other than confusing it is not nearly as bad as Coq in english.
Michael Soegtrop (Apr 06 2021 at 16:06):So how about officially naming it COQ with official pronunciation "See-Oh-Queue" any maybe as logo an Eye + O + some symbolic representation of a queue?
Michael Soegtrop (Apr 06 2021 at 16:06):I think that should clarify the pronunciation.
Yannick Zakowski (Apr 06 2021 at 16:20):All opinions set aside, do we have a good sense of how hard it would be to officially change the name in terms of labor, in terms of PR, and w.r.t. to Inria? And who has the authority to make the final decision about it?
Yannick Zakowski (Apr 06 2021 at 16:21):Because I have seen (and argued myself) opinions ranging from "it would be a PR nightmare" to "that's a trivial thing to do"
Yishuai Li (Apr 06 2021 at 16:24):One could fork the Coq repo and create an English-inclusive language called "Rooster" that is fully compatible with Coq.
Théo Zimmermann (Apr 06 2021 at 16:30):@Yannick Zakowski I'm not quite sure that what I'm going to say is correct, but I believe that the Coq development team has final say on the future of Coq, and that Inria would support the decision, whatever it is.
I'm personally more worried about the impact on the ton of preexisting work (in particular academic papers, books, etc.) which talk about Coq. And a lot of things are named after Coq (coq-community, MetaCoq, VsCoq, Coqtail, etc.). Some, like coq-community and MetaCoq even have nice logos already.
That's why I would favor a strategy that doesn't cut ties with this history (like the "Gallina / Coq" dual naming that I proposed in the Coq-Club discussion) or the recommended pronunciation strategy.
Yishuai Li (Apr 06 2021 at 16:37):We cannot predict whether a fine name or pronunciation today becomes offensive tomorrow. That's why I proposed "unspecifying" the official English representation, and allow anglophones do whatever they like.
Yannick Zakowski (Apr 06 2021 at 16:39):W.r.t. to historical naming of projects and the likes, a colleague (dunno if they wants to be named, they can denounce herself if they wish so :) ) has suggested to use Thierry's full name, Coquand. I wasn't convinced initially as it's a bit overly centered on Thierry Coquand, but it could solve the problem while making the cohabitation with "coq"-named repo easy as it's immediately identified with a shortened name
Théo Zimmermann (Apr 06 2021 at 16:42):Let's start collecting ideas for alternative names / pronunciations on a wiki page. When the name list is saturated, we can start doing a survey of the Coq community about this name changes (and other things, as it would be sad to waste effort on a survey with just one question) so we can eventually get to a decision.
Théo Zimmermann (Apr 06 2021 at 16:43):In particular, changing the logo now without knowing if the name is going to change would be a waste of time and money.
Théo Zimmermann (Apr 06 2021 at 16:43):I'll create the wiki page now.
Théo Zimmermann (Apr 06 2021 at 16:58):Here it is: https://github.com/coq/coq/wiki/Alternative-names
Emilio Jesús Gallego Arias (Apr 06 2021 at 17:04):That's a great idea Théo, I feel that indeed an alternative name _must_ have the property that somehow can be interchanged for Coq
Emilio Jesús Gallego Arias (Apr 06 2021 at 17:04):Like the proposals for C.O.Q.
Emilio Jesús Gallego Arias (Apr 06 2021 at 17:05):Regarding official name change I guess if the name is good enough that would not be a problem, but it is important that those outside France understand the context the name is used is actually quite positive, more in the sense of "we are proud, look at our rooster"
Emilio Jesús Gallego Arias (Apr 06 2021 at 17:05):It doesn't help that unless I am mistaken, no member of the Coq team is a native English speaker, thus we don't feel this issue so much and regular comm happens in French often
Théo Zimmermann (Apr 06 2021 at 17:05):Agreed with everything you said.
Théo Winterhalter (Apr 06 2021 at 17:06):Yishuai Li said:
We cannot predict whether a fine name or pronunciation today becomes offensive tomorrow. That's why I proposed "unspecifying" the official English representation, and allow anglophones do whatever they like.
I don't find this solution practical. If anyone can name Coq as they want, then how can you find resources about Roost or Rooster? The community is already divided around several platforms, I think it would be very hurtful to have several official names.
Yishuai Li (Apr 06 2021 at 17:10):Théo Winterhalter said:
I think it would be very hurtful to have several official names.
I'm proposing only one official name "L'Assistant de Preuve Coq" and all others are unofficial (e.g. Rooster, Coq证明助理, Coq定理证明器, Coq语言). Users should just learn one French word "Coq" to find all resources.
Emilio Jesús Gallego Arias (Apr 06 2021 at 20:50):Whoever is trolling the wiki is doing a nice job :)
Emilio Jesús Gallego Arias (Apr 06 2021 at 20:52):If C people named the successor as C++, what would be the successor of Coq featuring a more "advanced" type theory?
Yishuai Li (Apr 06 2021 at 22:34):Should the upcoming survey collect demographic information like first and second language (French/English/other)? I am observing active discussion in languages other than these two, and would like to offer Chinese translation for the survey.
Matthieu Sozeau (Apr 06 2021 at 22:57):We can certainly do that indeed, Yishuai.
Yishuai Li (Apr 07 2021 at 02:36):(deleted)
Fabian Kunze (Apr 07 2021 at 07:48):Btw, I think the name "Coq Club" is also unfortunate. One could interpret this as a place for dudes, and at least I never call it that, but "Coq mailing list", because of that.
Tadeusz Litak (Apr 07 2021 at 11:47):I can repeat what I already wrote in the mailing list.
While I was never happy myself with Coq's name and I understand people's concerns, anybody pushing for a drastic name change should think twice about all unintended consequences. The fact (pointed out by Emilio) that Coq's name appeals to French national pride may be more important than some people seem to appreciate. And besides, we're dealing with a massive legacy here.
If one really insists on changing the name, I find minor name modifications like "COQ", "Coq au... <French word of your choice>", "Côq", or "Le Coq" worth considering. Others seem non-starters. Just imagine "Gallus (Formerly Known as Coq)" or "Rooster (Formerly Known as Coq)". How would such choices be even innuendo-free?
And yes, the logo and the entire symbolism should remain rooster-based, perhaps just better designed.
Makarius Wenzel (Apr 07 2021 at 17:44):I am a foreigner on this channel, but we also have a proof assistant where the name is based on G. Huet --- the joke was made by his former office mate L.C. Paulson, not by Huet himself.
So from safe distance, here my proposals:
* Coquet, e.g. see https://fr.wikipedia.org/wiki/Lori_coquet
* Coquette or La Coquette, e.g. see https://fr.wikipedia.org/wiki/Coquette which lists birds, fish, and a film
k32 (Apr 07 2021 at 18:58):Just an observation: usually, when a non-English speaker raises a similar issue: "$name means something nasty in my $language", the issue is closed with answer "[WONTFIX] it's very funny".
Maxime Dénès (Apr 07 2021 at 19:16):Ok, but it is a fact that we're all using English as our communication language for work. And it's not like the name was chosen without being aware of the English meaning...
Maxime Dénès (Apr 07 2021 at 19:18):So maybe it is time to consider that a 30 year old joke has been making us laugh enough, that we can move on and pick a name better suited for an industrialization of the tool. Let's not forget that the original name was picked for a research prototype. It was hard/impossible to foresee that it would still be used today for a widespread tool.
Maxime Dénès (Apr 07 2021 at 19:22):As for the pride and legacy, I hope it is more based on the ideas promoted by Coq (dependent types, constructivism, formal proofs, etc) than the intended pun on the name of the tool and the resemblance with our national emblem :)
Matthieu Sozeau (Apr 07 2021 at 19:27):Haha, I was wondering when you were going to chime in Maxime :) It's not like you didn't warn us this would come again! I think now is as good a time as ever to change it.
k32 (Apr 07 2021 at 19:53):As a non-English speaker, I am not sure which is worse: an old joke or the risk of sending a message "all languages except English are irrelevant".
Enrico Tassi (Apr 07 2021 at 19:56):FTR, I was looking at what Coq would look like in esperanto, and it seems it's written "koko".
Enrico Tassi (Apr 07 2021 at 19:57):and its "voice" is "kokokri*", so nice ;-)
Matthieu Sozeau (Apr 07 2021 at 19:58):Yep, I like koko too.
Enrico Tassi (Apr 07 2021 at 19:58):In italian, the chicken does "cocode", but if I'm not mistaken the coq does "chichirichi" ;-)
(there is no k in italian, ch plays its role)
Matthieu Sozeau (Apr 07 2021 at 19:59):Rather than "all languages except english are irrelevant" the stance would be "english is the de-facto language of research and we should be extra-careful about it", IMHO
Matthieu Sozeau (Apr 07 2021 at 20:01):Don't get me wrong, I'm french and I love the Coq name, my phone is full of pictures of roosters to use in talks. But even that sentence is tendencious.
Matthieu Sozeau (Apr 07 2021 at 20:02):My girlfriend suggested "Codet" as in "Coq Coq Codet", but that's another french thing apparently
Enrico Tassi (Apr 07 2021 at 20:03):One thing that always pisses me off, is that .v is already taken by verilog... but maybe .k is not taken (yet)
Matthieu Sozeau (Apr 07 2021 at 20:03):Haha, github metrics getting you sad?
Enrico Tassi (Apr 07 2021 at 20:03):"cocode"
cousins ;-)
Enrico Tassi (Apr 07 2021 at 20:05):Maybe it's "coccode" in Italian, I'm loosing it, calling @Laurent Théry to the rescue
Emilio Jesús Gallego Arias (Apr 07 2021 at 20:40):@k32 unfortunately the problem is much worse than a joke, the meaning in English is sexual and pretty embarrassing, so indeed it is causing active harm for example in official conferences / activities, so a solution must be found.
Pierre-Marie Pédrot (Apr 07 2021 at 21:22):TIL @Enrico Tassi has been faking being an Italian for so many years.
Laurent Théry (Apr 07 2021 at 21:23):cocorico (in italian chicchirichi) is for the roaster, cot cot codet (coccode) is for the chicken.
Maybe we should try to be gender fluid, never knows :see_no_evil:
Pierre-Marie Pédrot (Apr 07 2021 at 21:23):His accent is fake as well and his real French can be traced backs to the suburbs of Ménilmontant
Emilio Jesús Gallego Arias (Apr 07 2021 at 22:03):By the way how does "CoqLang" sound to native speakers? We used this for twitter and if it sounds OK could be a good replacement for talks.
Jasper Hugunin (Apr 07 2021 at 22:14):(To my ear, anyways,) "CoqLang" is a slight to moderate improvement, especially if you blend the pronunciation in the middle. If someone asks you to say that again, or more clearly, you're back at the start. Maybe good for talks, where the audience can be expected to know what you are referring to, but not particularly helpful when talking with family or other lay people (or new students, for that matter) where you're particularly likely to be asked for a clear pronunciation of this new word.
Jasper Hugunin (Apr 07 2021 at 22:29):With "cocode", you are close to a neutral-connotation false cognate in Japanese, especially if you pronounce "code" as something like "co-day" (which is a natural sounding-out for Japanese phonology), it translates to "here", as in "things are happening here". It's not hard to make a slogan out of "here": "We do great things here", "Everything starts from here", etc. (student of Japanese, not a native speaker, so please correct me if I say something wrong).
Matthieu Sozeau (Apr 07 2021 at 22:31):Personally I find CoqLang and CoqTool to be too bland and I hope we can do better
Emilio Jesús Gallego Arias (Apr 07 2021 at 22:35):Matthieu Sozeau said:
Personally I find CoqLang and CoqTool to be too bland and I hope we can do better
I agree, it would be useful only as a short-term solution.
Laurent Théry (Apr 07 2021 at 23:47):@Matthieu Sozeau @Enrico Tassi I like koko too but written Coq-O
Enrico Tassi (Apr 08 2021 at 06:23):One more point for Koko : it's also the name of the gorilla to hat could talk https://en.m.wikipedia.org/wiki/Koko_(gorilla)
Enrico Tassi (Apr 08 2021 at 07:19):I've added koko to the wiki page
Jean-François Monin (Apr 08 2021 at 09:59):Some people just don't want to pronounce coq in a number of circumstances and basically outside our community (for lack of proper background). On the other hand I don't see the point of changing coq in written things (papers, commands, tools, etc.). Is it not possible to keep writing coq in knowledgeable circles and stick to a neutral acronym such as CPA (coq proof-assistant) for other audiences ? A number of acronyms are already commonly used (e.g., LASER).
Matthieu Sozeau (Apr 08 2021 at 10:04):That would be an ideal solution because it would be lightweight to implement, however the chosen name should eventually shadow the original otherwise the problem remains I believe.
Théo Zimmermann (Apr 08 2021 at 10:20):Yes, I like the proposed Copa (also short for Coq proof assistant) for this reason. But IMHO we need to start to use it also in our own community (even if we could then keep the command-line tools unchanged). Otherwise, it's no use talking about it to external people. What if they then start looking for it on the web and do not find anything related to it?
Enrico Tassi (Apr 08 2021 at 10:24):Copa is both an airline and a football merchandise shop
Yannick Forster (Apr 08 2021 at 10:25):And the name of some more things: https://en.wikipedia.org/wiki/Copa
Dan Frumin (Apr 08 2021 at 10:55):Matthieu Sozeau said:
Personally I find CoqLang and CoqTool to be too bland and I hope we can do better
FWIW from my pov those names are even worse, "Lang" sounds too much like "length" in some accents. As for "CoqTool"... I mean if someone makes an association on the first part of that word, than they can easily use the second part to strengthen the innuendo.
Lélio Brun (Apr 08 2021 at 13:05):Enrico Tassi said:
One more point for Koko : it's also the name of the gorilla to hat could talk https://en.m.wikipedia.org/wiki/Koko_(gorilla)
It also means vagina in Haitian kreyol... Not sure if a lot of Haitians or people of Haitian descent use Coq though, even taking the diaspora into account.
Matthieu Sozeau (Apr 08 2021 at 13:29):Koko has a lot of friendly connotations in french but also a political one (phonetically, it's slang for communist)
Théo Zimmermann (Apr 08 2021 at 14:36):That's still a friendly connotation though, isn't it? :stuck_out_tongue:
Matthieu Sozeau (Apr 08 2021 at 16:04):Depends who says it, as always ;)
Dan Frumin (Apr 08 2021 at 17:25):Théo Zimmermann said:
That's still a friendly connotation though, isn't it? :P
Perhaps for residents of capitalist countries
Théo Zimmermann (Apr 08 2021 at 17:28):Indeed, I meant specifically in France (because coco is a shorthand for communist in French).
Guillaume Claret (Apr 08 2021 at 17:59):The website for Coq Club seems down: https://sympa.inria.fr/sympa/arc/coq-club
Tadeusz Litak (Apr 08 2021 at 20:04):Théo Zimmermann said:
Indeed, I meant specifically in France (because coco is a shorthand for communist in French).
Having been born in a communist country, I wouldn't appreciate at all if Coq's developers deliberately chose a new name with such connotations. This is one point where the French academic sensibility and those of Central-Eastern Europe would diverge dramatically (you can also include Taiwanese or Caucasian experiences, or those of Cuban or Saigonese immigrants in the States, and many other ones you haven't probably thought of). And I would be vocal about it.
It might seem funny to you. Rest assured that for many people it seems much less funny than even penis jokes.
Guillaume Claret (Apr 08 2021 at 20:11):A discussion is ongoing on Hacker News: https://news.ycombinator.com/item?id=26738980 (unfortunately most people have not been able to access the mailing list, as it seems it went down quite fast)
Talia Ringer (Apr 08 2021 at 22:40):ohhh this is why coq-club went down?
Talia Ringer (Apr 08 2021 at 22:41):Maybe this is also why random men are attacking me on Twitter
Talia Ringer (Apr 08 2021 at 22:47):lol this ridiculous conversation on HN, who are these people
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:48):@Talia Ringer if any of these "men" happen to be part of the Coq community in any way, please don't hesitate to contact the Coq's CoC team (regardless of the attacks happening on twitter) so they can take appropriate action. I'd be happy to help with that if you are tired of that.
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:48):I have no idea myself about hacker news , never been there other than the random link, interesting indeed.
Talia Ringer (Apr 08 2021 at 22:49):thanks. yeah it's usually a kind of awful place though there are interesting posts about technical work
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:52):But indeed I was surprised to see how much resistance is there. There will be resistance because if you forget about the "cock" problem, Coq is a pretty good and catchy name :/
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:52):And in French just perfect.
Talia Ringer (Apr 08 2021 at 22:52):Yeah but it's mostly just people projecting politics onto it
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:52):There is some context about _when_ Coq was named tho that IMHO is not so clear in the twitter trhead
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:52):and actually most of us were not even born
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:53):you need to place yourself in 1980
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:53):where "Political Correctness" started to be a thing
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:53):in particular "American Political Correctness"
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:53):and there was a huge pushback from Europe, not unanymous tho
Talia Ringer (Apr 08 2021 at 22:53):I also gave a job talk yesterday, an academic job interview, with automatic captioning for everyone watching, and it transcribed "the proof assistant called Coq" as "the persistent cold cock" for everyone watching
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:53):mixed with the perceived "americazation" of European culture
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:54):Talia Ringer said:
I also gave a job talk yesterday, an academic job interview, with automatic captioning for everyone watching, and it transcribed "the proof assistant called Coq" as "the persistent cold cock" for everyone watching
That's a serious problem, indeed I am not using Coq in any talk more or less public and not targetted to French
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:54):I will use Rooster
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:54):which is IMO super acurate, because as French speakers this is what we understand
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:55):but Coq is catchy for marketing
Talia Ringer (Apr 08 2021 at 22:55):That's interesting
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:56):But yeah that is so complex
Talia Ringer (Apr 08 2021 at 22:56):I do appreciate how constructive and kind the main Coq developers have been, and the democratic and community-based approach to this
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:56):I'd bet that many of the negative reactionaries on HN are coming from that point of view, the same history about "americanization" / "globalization" again
Talia Ringer (Apr 08 2021 at 22:56):It's just occasionally awful people who start attacking me for even saying "hey like maybe it's not great when talking about my life's work in public puts me in awful situations"
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:56):we'd get into politics and that's a hairy topic and Inria's desire is that at least officially we don't get involved into them
Talia Ringer (Apr 08 2021 at 22:57):yeah i have trouble understanding that whole debate
Talia Ringer (Apr 08 2021 at 22:57):i'm very culturally israeli, was not exposed to dominant american culture until college, just grew up among a big israeli community in the US
Talia Ringer (Apr 08 2021 at 22:57):political correctness isn't a thing in israel, everyone just says exactly what they think always
Talia Ringer (Apr 08 2021 at 22:57):I just don't like getting harassed and I don't like students feeling bad about this kind of thing, I think that's fair
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:57):Talia Ringer said:
yeah i have trouble understanding that whole debate
Yeah the political debate is complex, however there is a real an urgent problem with the name, I'm picking the Rooster solution myself, I don't want to keep saying "Coq" to people that will understand cock
Talia Ringer (Apr 08 2021 at 22:58):I want people to be able to Google it and find it
Talia Ringer (Apr 08 2021 at 22:58):because I care about growing the community
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:58):https://www.google.com/search?q=rooster+theorem+prover :)
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:59):That is not a long-term solution, but I like it because now my brain maps French to English
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:59):when I speak French I say Coq I mean Rooster
Emilio Jesús Gallego Arias (Apr 08 2021 at 22:59):so it kinda fits nice in my brain
Tadeusz Litak (Apr 08 2021 at 22:59):Emilio Jesús Gallego Arias said:
I will use Rooster
I am not exactly convinced that, say, "Little Red Rooster" is a song about sustainable farming. And let me point out again: if an alternative name is adopted, be prepared that it will be often accompanied by "... (Formerly Known as Coq)". Not even to tease anybody, simply for clarity. But the final effect might not exactly be innuendo-free.
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:00):Hi @Tadeusz Litak , I am not proposing Rooster as the new name, but just as my own personal workaround as indeed when I was in the US Coq led to awkward situations
Talia Ringer (Apr 08 2021 at 23:00):woah that's cool that it translates on Google
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:01):For example I felt uncomfortable talking about Coq when I worked in the US to studends, specially female ones, stuff like "nice job with Coq"
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:02):feels awkard, so I will personally translate
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:02):until a new name is chosen
Talia Ringer (Apr 08 2021 at 23:02):Yeah so I just like, I totally forget in most contexts, I'm so used to saying Coq. But this is actually what's dangerous about it. I find myself in public, in restaurants for example, and I say "I'm a Coq expert" or "my life's work is Coq" or whatever and the best outcome of that is extremely dirty looks
Talia Ringer (Apr 08 2021 at 23:03):Like talking to other people I'm out with (this is pre-pandemic obviously)
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:03):I'm a Rooster expert would be interesting, this is what French understand :)
Talia Ringer (Apr 08 2021 at 23:03):Honestly much better outcome, probably
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:04):"I'm a theorem proving expert" seems quite better in that context tho.
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:05):unless people is super expert they have no chance to know coq
Talia Ringer (Apr 08 2021 at 23:06):Yeah the problem is that because I always call it Coq in technical contexts, I just naturally call it Coq everywhere
Talia Ringer (Apr 08 2021 at 23:07):Like, actually, if someone says "cock" to me, I will probably hear "Coq" and think they are talking about the proof assistant
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:07):By the way to clarify a few things I saw on twitter and in other places, Coq was named after Coquand (obviously because he solved an extremely important and famous open problem with the SN for CoC, there are many anecdotes about that) the rest is kind of accessory; sometimes I have gotten the impression that people were claiming that Coq was name to bother the americans, this is just not factually true, even if they were not unhappy about it at all tho :)
Talia Ringer (Apr 08 2021 at 23:07):But for a woman in the US, this is awkward at best and unsafe at worst
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:07):Talia Ringer said:
But for a woman in the US, this is awkward at best and unsafe at worst
That is clear.
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:08):That's why I am stopping all use right now.
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:08):Except in France
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:08):and in the community
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:08):or maybe I call it R/C
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:08):Rooster/Coq
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:08):in the talks, we will see when I have to present in English again
Talia Ringer (Apr 08 2021 at 23:11):Whatever it is, I'm all for preserving the legacy of the name as much as possible, and I honestly didn't mind the "Coquand" suggestion with the caveat that one person mentioned it's weird since he's still alive
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:12):"Coquand" is not bad at all, tho awkward indeed.
If finding a new name works it will prove that crowdsourced CS is possible, because this problem seems hard enough for an A+ conf [consensus, logic, semantics, natural lang, ... XD]
Emilio Jesús Gallego Arias (Apr 08 2021 at 23:13):Ok gonna get going, take care and best of luck with your job search!
Talia Ringer (Apr 08 2021 at 23:24):Thanks!
Tadeusz Litak (Apr 08 2021 at 23:29):I am also tired of constantly saying "The Coq Proof Assistant" instead of just "Coq" in most contexts to soften the impact. And in more conservative cultures the situation might be much worse. I wish that people paid more attention to the email of Wilayat Khan, who described how bad the effect on students and the academic community is in India or Pakistan.
All that I am saying is that while this is a suboptimal situation and it'd be great to find a sensible, non-invasive remedy, there won't be an easy one, and unintended consequences will be serious, one way or another. One often has to choose between unappetizing and unacceptable. The challenge is to figure out which is which.
And I'll say again: why Emilio mentioned the funding factor in passing, it seems supremely important to me. Quite honestly, if the entire world outside of France would cease to use Coq, it would probably still survive (even if horribly crippled). But without French institutional support, it is not going to survive long. So every step that could potentially lead to diminishing of that support is very dangerous. I trust in the good sense of the developer team, but I do hope this is always kept in mind.
Xuanrui Qi (Apr 09 2021 at 07:01):If I'm not talking to a technical audience, I prefer not to talk about the name of the thing I'm working on, simply because it's overly specific and not necessary. I usually say something that "I work on a piece of computer software that can check mathematical proofs", etc. Maybe that's a good strategy at the moment.
But indeed a non-invasive remedy is required.
Théo Zimmermann (Apr 09 2021 at 08:48):So every step that could potentially lead to diminishing of that support is very dangerous. I trust in the good sense of the developer team, but I do hope this is always kept in mind.
Don't worry this will be kept in mind. My own position is on a fixed-term contract and my future employment at Inria probably depends on that renewed funding.
Théo Zimmermann (Apr 09 2021 at 08:51):@Tadeusz Litak Also, I'm sorry for upsetting you with respect to the communist slang in French. I do recognize the horrible impact of communism in many countries. I was just thinking that the confusion was not important because it would only happen in French, and in France communism was never a threat and the communist party is a very small and "normal" left-wing party today. But after all this discussion, it seems that choosing "koko" as the new name could risk sending the wrong signal.
Théo Zimmermann (Apr 09 2021 at 08:54):(Most young French people probably don't even know that "coco" is a shorthand for "communist" since it has become of so little political importance.)
Théo Winterhalter (Apr 09 2021 at 08:55):The first thing that comes to mind is the coconut to be honest.
Pierre-Marie Pédrot (Apr 09 2021 at 08:56):Am I the only French person in that demographic group that thinks about the Minikeum Coco, who is supposed to be a parody of Antoine de Caunes?
Théo Winterhalter (Apr 09 2021 at 09:06):Pierre-Marie Pédrot said:
Am I the only French person in that demographic group that thinks about the Minikeum Coco, who is supposed to be a parody of Antoine de Caunes?
I was too young to understand the reference. But I did watch Coco and co.
Gaëtan Gilbert (Apr 09 2021 at 09:19):Quite honestly, if the entire world outside of France would cease to use Coq, it would probably still survive (even if horribly crippled). But without French institutional support, it is not going to survive long.
These are not independent factors, the institutions care about international reach.
Matthieu Sozeau (Apr 09 2021 at 10:51):@Pierre-Marie Pédrot thanks for reminding me I forgot about that one :)
Pierre-Marie Pédrot (Apr 09 2021 at 11:00):It so happens that there is also a Minikeum Gégé (Gérard [Depardieu, not Huet]). Here is for instance a video where you can see both at the same time.
Aloïs Cochard (Apr 09 2021 at 12:52):Coq-O-vin
Théo Zimmermann (Apr 09 2021 at 14:28):I like the proposal added by @Clément Pit-Claudel of renaming Coq into "Rocq" very much. Besides all the already listed advantages (https://github.com/coq/coq/wiki/Alternative-names#rocq), it is pretty much associated with the idea of resisting American imperialism. For those who do not know the story, INRIA-Rocquencourt (the place where Coq was born) was created on a former US military base after de Gaulle decided to kick US military out of France.
Emilio Jesús Gallego Arias (Apr 09 2021 at 14:48):That's a pretty good one indeed, "My proof is Rocq solid!"
Meven Lennon-Bertrand (Apr 09 2021 at 14:49):And Inria can keep on with the avian jokes for a few more decades (if there are still any left)
Enrico Tassi (Apr 09 2021 at 14:51):Rocq and roll
Guillaume Claret (Apr 09 2021 at 15:32):to me this is more a disadvantage this story (resisting American, I do not even know if this was a good idea); also a Rocq is more associated to a rock, which is less poetic than a bird
Talia Ringer (Apr 09 2021 at 18:08):Rocq and Coquand are my two favorites right now. I think keeping it as French as possible is ideal, and the deliberate reference to resisting American imperialism in Rocq is a funny way to do that, but one I don't find inappropriate.
Talia Ringer (Apr 09 2021 at 18:09):Honestly thanks for even having this discussion so seriously, whatever happens
Talia Ringer (Apr 09 2021 at 18:10):I do suggest that when you eventually send out the survey, you find a way to avoid trolling from outsiders---if this got posted to HN, very well the survey may also get posted to HN. I don't know how to control this well while maintaining anonymity and opening it up to everyone, but it's worth taking really seriously.
Talia Ringer (Apr 09 2021 at 18:12):As always, my experiences with the core group of Coq developers remain super positive :big_smile: even if this doesn't lead to a meaningful change, the seriousness with which it is being considered is wonderful
Bas Spitters (Apr 09 2021 at 18:39):My non-PL colleagues are wondering what is going on with all the memes. I had to explain them a 35yr old French jab at american cultural imperialism :-(
I don't have anything to add to the discussion.
Joshua Grosso (Apr 09 2021 at 19:06):Minor point: As an anglophone, I wouldn't be sure just by reading how to pronounce "Rocq" ("rock"? "rock-queue"?); "Roc" and "Roq" are more obvious, for me at least.
Matthieu Sozeau (Apr 09 2021 at 20:06):That's a quite interesting proposal, I like it !
Tadeusz Litak (Apr 09 2021 at 21:13):Let me drop my usual fly into this ointment. After such a renaming, it would often get referred to as "Rocq/Coq". Not sure if I am the only person who sees dangers in this.
Jasper Hugunin (Apr 09 2021 at 21:35):The situations where a "(formerly known as Coq)" suffix would be appended to a name are different than the ones where harassment has been publicly reported. If I was talking to family or other lay people, I would just use the new name; they are not familiar with the system when it was called Coq, nor do they have a particular need to link the histories. Similarly, when speaking to a class of students, there doesn't seem to be any need to lead with the history of the name: the system they will be learning about is now called whatever the new name is. Casual conversation with other Coq users is similar: there is no need to bring up the old name every time the name is used because both parties already know the history. When writing papers about Coq, such a qualification is probably important to connect the histories, but Coq is much less problematic for English speakers in writing than when speaking. Similarly, if giving a talk, the "(formerly known as Coq)" could reasonably be relegated to a footnote on the slides, and not spoken.
Tadeusz Litak (Apr 09 2021 at 21:39):All valid points, but this particular name also invites other puns such as "Rocq-hard proofs".
Jasper Hugunin (Apr 09 2021 at 21:39):I haven't seen in the discussions anyone giving a reason that we need to find a name which cannot be interpreted offensively even if you try. The problem that we seem to be trying to address is that the current name requires a certain amount of maturity not to interpret offensively, which is unfortunately too much to expect from every random stranger, who then cause harm to members of our community.
Talia Ringer (Apr 09 2021 at 22:16):Thanks Jasper for the great answers there :big_smile:
Rebecca Turner (Apr 09 2021 at 22:40):Just chiming in to say that I was glad to see the announcement about renaming Coq and especially as a female student to see my experience (being put off by / not learning Coq because of its name) be acknowledged. Best of luck to everybody in choosing a new name! :tada:
Joshua Grosso (Apr 10 2021 at 03:46):I'm just curious: Have we all considered having the official pronunciation be language-dependent? (So in French, you'd pronounce it correctly, and in English, you could pronounce it e.g. "coke"?)
Joshua Grosso (Apr 10 2021 at 03:47):Because it seems to me that changing the pronunciation of an existing French word across-the-board is kinda silly (assuming the spelling doesn't change as well), but if the change is localized to English, we might be able to have our cake and eat it too.
Jasper Hugunin (Apr 10 2021 at 04:24):Yes, changing the pronunciation when speaking in English has been mentioned, both on the original email thread and on the wiki. The first section of the wiki page "Alternative pronunciation strategies" is focused on these, feel free to add on to the discussion there!
Marco Paviotti (Apr 10 2021 at 14:30):(deleted)
Marco Paviotti (Apr 10 2021 at 14:31):Hello everyone, I am not much of a coq expert but i thought i would just put my two pennies in. I don’t think just changing the pronunciation or turning Coq into Coc / Kok would change much since Coq per se gets pronounced as cock anyway. I would be happier with a more stark change. Of the names that have been proposed CiC (pronounced Kick) is a good name in my opinion. It stands for Calculus of Inductive Constructions and the recursive variant CiC is Coq.
Tadeusz Litak (Apr 11 2021 at 01:42):Elaborating on variants of "Cockatrice": would "Coquandrix" have any takers? It's the monster begot by Coquand and hatched from Coq’s egg. The glance of its eye sufficeth to turn to a rocq-solid proof any living thing that standeth before it. An attempt to look at itself in the mirror (prove its own consistency) would immediately kill it though. Added to the wiki, just in case.
Tadeusz Litak (Apr 11 2021 at 01:48):Other less advertised proposals from the wiki that I like include also Coqpit and Coq n'œuf (Coq neuf, Coq9). And of course TPAFKAC.
Tadeusz Litak (Apr 11 2021 at 06:42):Coming back to the issue of X Formerly Known As Coq, nobody says that using the old name would be necessary for uniqueness. This is a straw man. The point is that human brain doesn't work like a computer. If you used the old name for years, you're going to find yourself slipping back to it for a really long while: in lectures, talks and above all in casual conversations. Especially so if that banned name still persists in thousands of papers, files and repositories, in books, teaching materials, tools, blogs, citations, videos and where else, as the name of Coq would.
So if the new name would create a provocative clash with the old one, good luck.
This is also why (even if the extremely risky decision to change the name is made), I would find not keeping "Coq" a (semi-)officially endorsed abbreviation self-injury and an own goal.
Clément Pit-Claudel (Apr 11 2021 at 16:25):Tadeusz Litak said:
Let me drop my usual fly into this ointment. After such a renaming, it would often get referred to as "Rocq/Coq". Not sure if I am the only person who sees dangers in this.
Tadeusz Litak said:
All valid points, but this particular name also invites other puns such as "Rocq-hard proofs".
Tadeusz Litak said:
So if the new name would create a provocative clash with the old one, good luck.
Maybe I'm not sufficiently up-to-date on slang, but what bad connotations do "Rocq/Coq" and "rock-hard proofs" have? When I look up "rock hard" in Google it gives me 4x4 ads and a German music magazine. I get that "rock hard" means "very hard", so it could be applied in an explicit context, but does it carry an explicit connotation on its own? About "Rocq/Coq" I find lots of references to the Andean Cock of the Rock bird ("rupicola"), and a wikipedia page on a music style with an explicit name, so I guess we might worry about "Coq/Rocq" (?), but I don't see the issue with "Rocq/Coq"?
(FWIW, I think this is stretching it: the problem with the current name is a lot more serious than "the name can be combined with other words to make an explicit joke", and I fear that it'll be extremely hard to find a name that cannot be combined in such a way — meanwhile, Rock on its own has lots of positive connotations)
Tadeusz Litak (Apr 11 2021 at 16:54):Native speakers can correct me on this, but I believe that "rock-hard" is an adjective commonly associated with an erection. Numerous rock hits are playing on this pun: Suzi Quatro's "Rock Hard", Kiss' "(You Make Me) Rock Hard", AC/DC's "Hard As A Rock" seem the first results of a Google Video search for the phrase (check the lyrics to those and similar songs). You can also try this:
https://duckduckgo.com/?q=rock-hard&t=brave&ia=web
(Top hits include "Rock Hard Pills Review", "How to Get Rock Hard Erections", "How to Get Harder Erections", "Alpha Rock Hard Formula Reviews")
The word "rock" in itself of course has a lot of other very positive associations. But when you slip in the middle of a sentence and replace "rocq" with "coq" and then try to correct yourself, the unintended associations might be hard to avoid. Perhaps it works differently with the younger generation, I don't know.
Matthieu Sozeau (Apr 11 2021 at 18:14):I feel this is stretching it too, Rocq by itself isn't offensive, if you just say it to someone who doesn't know about it, I don't see it getting misinterpreted. It also has good connotations and references. We should certainly discourage Rock/Coq (or any "formerly known as" variant). Of course there is rock hard, but also rock around the clock, rock'n'roll, etc... at some point we can't control how the name will be used in any context.
Matthieu Sozeau (Apr 11 2021 at 18:16):Also, people use "hard as a rock" in completely innocent contexts, no?
Théo Winterhalter (Apr 11 2021 at 18:33):I believe that in this context it is "hard" which on its own already carries the meaning of "erected". I mean, a rock is a rock.
I don't particularly like the name, but I don't think we can avoid misuse in a sentence for pretty much any word.
Jasper Hugunin (Apr 11 2021 at 18:53):Yeah, as a native speaker "rock hard" isn't particularly suggestive without a suggestive context (or applied as an adjective to a male person), and this particular phrase doesn't seem particularly likely to come up in conversation when Rocq is a name. "Rocq solid" also sounds like the more natural phrase when used to describe a proof or a safety guarantee, and that is even less suggestive.
Jasper Hugunin (Apr 11 2021 at 18:57):And "rock" on it's own isn't a synonym for "cock" to the extent of my knowledge, so if I hear "... and so I was using Coq last night, sorry, no, it's called Rocq now, ..." the correction doesn't increase the suggestiveness of the original slip-up to my ear.
Jasper Hugunin (Apr 11 2021 at 18:59):"rock hard" can also be used to refer to muscles: arm muscles, stomach muscles, "rock hard body", etc. and is a positive for male beauty standards only tangentially related to sex.
Talia Ringer (Apr 11 2021 at 19:05):Yeah when I hear "rock hard" my brain autocompletes it to "abs" which is fine haha
Bas Spitters (Apr 11 2021 at 19:36):Rupicola is a beautiful name for coq/rock, but it's taken ...
https://en.wikipedia.org/wiki/Andean_cock-of-the-rock (rupicola)
https://github.com/mit-plv/rupicola/
Joe Hendrix (Apr 11 2021 at 20:05):As a non Coq user who nevertheless needs to mention Coq to people unfamiliar with it, I'm pretty supportive of the name change. I usually end up saying the "Coq Theorem Prover" or something similar.
Since it looks like a new name is strongly being considered, I'd just recommend folks explicitly ask friends from cultures underrepresented in the current user base what they think of the name.
For example, I'm an American and the name Rocq seems good to me in that it is not embarrassing while still be slightly awkward enough to figure out how to pronounce to suggest the French origin. :) On the other hand, I know native Chinese and Japanese speakers sometimes have trouble with the L/R distinction and words that end in a consonant. I think Rocq isn't terrible for native speakers of east Asian languages, but that reminded me that if the community is going to change the name, it'd be good to get a diverse set of speakers providing input.
Tadeusz Litak (Apr 11 2021 at 21:04):Matthieu Sozeau said:
We should certainly discourage Rock/Coq (or any "formerly known as" variant). Of course there is rock hard, but also rock around the clock, rock'n'roll, etc...
Good luck with discouraging such variants, Matthieu...
I tried DDG with several locations on moderate settings. This is the first hit for "rock cock" that I can share at all (still with a trigger warning):
https://www.urbandictionary.com/define.php?term=rock%20cock
Meanwhile, this is the first hit for "cock rock", which confirms that rock music associations are rather problematic in Coq's context:
https://en.wikipedia.org/wiki/Cock_rock
Anyway, if I am the only person who sees a problem here, let's rocq!
Gaëtan Gilbert (Apr 11 2021 at 21:32):Do other X cock queries really do better?
Clément Pit-Claudel (Apr 11 2021 at 21:34):@Tadeusz Litak look it up on google rather than on Urban Dictionary: Rock Cock:
image.png
In other words, "rock cock" almost universally means the bird, as far as I can tell, not something explicit
Tadeusz Litak (Apr 11 2021 at 21:38):Google searches are more heavily curated and censored than those of DuckDuckGo (that's where the Urban dictionary entry came first... after more explicit stuff), so I am not sure if this hit is really most representative of associations that would arise. But as I said, if I am the only one raising such objections, and if native speakers see no evil and hear no evil, do go ahead.
Tadeusz Litak (Apr 11 2021 at 21:56):Gaëtan Gilbert said:
Do other
X cockqueries really do better?
This is exactly the point that I've been trying to make for quite a while (but I do promise to stop soon, if others see no issue here, I do have better things to do).
I believe you should not try to replace Coq's name with something else, especially not with anything which does not start with "Coq". If Coq's present name is not kept as a (semi-)official abbreviation, if you say it's banned, politically incorrect, and should not be used, you risk getting into a mess which is several times worse than the present one. You are not going to prevent the two terms from coexisting in the community, or even inside your own brain.
This is precisely what happened to XVIIIth-century American Puritans who originally introduced "rooster" to replace "cock", as somebody very adequately pointed out in the wiki. Increasingly, not only "cock" got much more pornographic in American English than in British English (at present, everybody got sufficiently influenced by AmEnglish for this distinction to disappear), but even "rooster" itself took on distinctly sexual undertones.
But I do hope to be the one in the wrong. If nobody else agrees with me, I am probably in the wrong. Let's simply go ahead.
Matthieu Sozeau (Apr 11 2021 at 23:57):I kind of agree a bit that "only a name change" is probably not sufficient to change minds, but if we do propose a sufficiently different version of the system (say, without a big part of the compability baggage we currently have), it might be a way to make the distinction clearer in everyone's minds (including mine :)
Yishuai Li (Apr 12 2021 at 01:37):I'm looking forward to a brand new version of the system called, say, CIC "CIC Isn't Coq".
Théo Zimmermann (Apr 12 2021 at 07:45):You can see horrifying results to the query "rock cock" on Google too if you disable the filters. But from what I can tell, you get the same with the query "cock" alone. "rock" isn't responsible for any of it.
Thomas Burdick (Apr 12 2021 at 09:52):I hope everyone involved in this name change is prepared for the next one in another 5-10 years. None of the people who are so horribly offended are arguing in good faith. The US goes through these witch hunts periodically, and has done for hundreds of years now. The only sensible thing to do is ignore them.
Tadeusz Litak (Apr 12 2021 at 12:15):Yishuai Li said:
I'm looking forward to a brand new version of the system called, say, CIC "CIC Isn't Coq".
Wouldn't it be CINC or perhaps CAC (CAC Ain't Coq)?
But it would be sufficient to call it Coq9 then and announce it's pronounced as "Coq n'œuf/neuf".
Théo Winterhalter (Apr 12 2021 at 12:19):One thing to take into account as well, is that changing the name too much will mean renaming a lot of tools right?
Théo Zimmermann (Apr 12 2021 at 12:23):Théo Winterhalter said:
One thing to take into account as well, is that changing the name too much will mean renaming a lot of tools right?
Yes, that was my initial reason for wanting a name that didn't depart too much from the current one. But if we do change the name to something that doesn't contain "Coq", it will be up to the tools / library maintainers to decide what to do with their name.
Théo Winterhalter (Apr 12 2021 at 12:24):I guess MetaCoq will have to change.
Yannick Forster (Apr 12 2021 at 12:26):Unless we rename the project but not the implementation (not to argue for this, but it's an option I guess). I could get used to saying MetaRocq though :)
Yannick Forster (Apr 12 2021 at 12:27):If the Coq9 idea gains support there might also be the related option to drop both version 9 and the pun and go with CoqX, pronounced Cox
Théo Zimmermann (Apr 12 2021 at 12:27):Yes, MetaRocq and rocq-community sound nice. But I guess Coquelicot and Coqtail won't change names.
Théo Winterhalter (Apr 12 2021 at 12:28):Yannick Forster said:
If the
Coq9idea gains support there might also be the related option to drop both version 9 and the pun and go withCoqX, pronouncedCox
A mix between Microsoft and Apple naming strategy.
Théo Winterhalter (Apr 12 2021 at 12:28):I don't know what Jesper Cockx will think.
Enrico Tassi (Apr 12 2021 at 12:29):Given the success of plan9, I'd rather avoid coq9 (a bit of trolling here)
Tadeusz Litak (Apr 12 2021 at 12:30):Théo Winterhalter said:
One thing to take into account as well, is that changing the name too much will mean renaming a lot of tools right?
Yes, and as I said above, you wouldn't remove Coq's name from thousands of papers, files, repositories, books, teaching materials, blogs, citations, videos etc.
It amazes me how quickly these considerations went out of the window.
Enrico Tassi (Apr 12 2021 at 12:32):Well, you can't change the past.
Emilio Jesús Gallego Arias (Apr 12 2021 at 12:33):"Coq 9 for Outer Space"
Enrico Tassi (Apr 12 2021 at 12:37):Proof General -> Major Tom
Tadeusz Litak (Apr 12 2021 at 12:38):Yannick Forster said:
If the
Coq9idea gains support there might also be the related option to drop both version 9 and the pun and go withCoqX, pronouncedCox
This sounds like "cocks", not to mention that "Cox" is already used in other contexts. See for example:
https://en.wikipedia.org/wiki/Cox_Communications
Bas Spitters (Apr 12 2021 at 12:41):There are many rooster pun project names: oueff (at least twice), quickchick, rupicola, ...
Perhaps they should also be collected on the wiki.
Yannick Zakowski (Apr 12 2021 at 12:42):(What is "oueff" a pun with?)
Gaëtan Gilbert (Apr 12 2021 at 12:54):oeuf maybe
Yannick Zakowski (Apr 12 2021 at 12:56):Oh of course that's probably it, I was stuck pronouncing the "ou" the usual French way. Thanks!
Gaëtan Gilbert (Apr 12 2021 at 12:57):I think Bas just typoed
Théo Winterhalter (Apr 12 2021 at 12:58):Enrico Tassi said:
Given the success of plan9, I'd rather avoid coq9 (a bit of trolling here)
We can always write "coq-neuf".
Théo Winterhalter (Apr 12 2021 at 12:58):I did not suggest coq9 because I wanted coq-neuf to mean both coq nine and new coq.
gallais (Apr 12 2021 at 13:22):Théo Winterhalter said:
I don't know what Jesper Cockx will think.
He's already jokingly using the handle agdakx to remove any doubts wrt his affiliation :laughter_tears:
Tadeusz Litak (Apr 12 2021 at 13:54):Yet another famous Cox:
https://www.imdb.com/title/tt0841046/
The surname seemed chosen also because of the potential for puns, and it is exploited (slightly less explicitly than with "cock") on several occasions in the movie.
Clément Pit-Claudel (Apr 12 2021 at 15:55):Thomas Burdick said:
I hope everyone involved in this name change is prepared for the next one in another 5-10 years. None of the people who are so horribly offended are arguing in good faith. The US goes through these witch hunts periodically, and has done for hundreds of years now. The only sensible thing to do is ignore them.
I know one's not supposed to feed the trolls, but let me attempt an answer, as a foreigner who's sometimes a bit lost in US cultural issues. The problem here is a touch more subtle than usual.
People are not only telling us that the name is making them, personally, uncomfortable (a few people might have said this, but I don't think anyone really has claimed to be personally "horribly offended" by the name Coq).
No, people are instead telling us 1. that the name forces them to make other people uncomfortable, for example while teaching or while discussing the system with people who are not Coq experts, to the point that they sometimes avoid teaching or discussing Coq; and 2. that using the name exposes them to mockery, and even in some cases to harassment.
These two points are serious. Add to this the fact that this is not just feedback from people outside of our community, from "outsiders" whose opinion we could just chose to dismiss: valuable, respected members of our community are telling us that a decades-old joke is creating significant difficulties for them. The least we owe them is a sincere discussion, and I personally trust multiple of the voices on the mailing list sufficiently to assume good faith.
In fact, I find it particularly odd to claim that "None of the people who are so horribly offended are arguing in good faith", given that people who shared uncomfortable experiences with the name "Coq" did so with remarkably little arguing (what I saw on the mailing list was mostly people sharing facts).
Oh, and FWIW: if we decide to rename Coq into "Capybara" and in 10 years English or French evolves in such a way that "Capybara" starts to make a significant number of members in our community uncomfortable, then I'll be in favor of considering a name change again. In the meantime, Rocq on :rock_on:.
Talia Ringer (Apr 12 2021 at 17:02):Yeah word, if I and others propose all of our points and some good names and insiders in the community overwhelmingly vote against a name change, I'm pretty sure I'll accept that outcome and look for more workarounds like different pronunciations for English-speaking researchers (this just seems harder to do well)
Wolf Honore (Apr 12 2021 at 18:38):Théo Zimmermann said:
Yes, MetaRocq and rocq-community sound nice. But I guess Coquelicot and Coqtail won't change names.
Coqtail -> On the Rocqs?
Tadeusz Litak (Apr 12 2021 at 20:20):Théo Zimmermann said:
You can see horrifying results to the query "rock cock" on Google too if you disable the filters. But from what I can tell, you get the same with the query "cock" alone. "rock" isn't responsible for any of it.
I searched DuckDuckGo on moderate settings. I didn't even see a point in checking what happens if filters are completely off. "Rock cock" does sound worse than just "cock" to me.
Tadeusz Litak (Apr 12 2021 at 20:25):If Coq is overhauled to a new version, partially incompatible with the present one, this "Rocq/Coq" combination would be even more likely to pop up. Perhaps not among Co..., pardon me, Rocq core user group, but among casual users and in the broader community.
Guillaume Claret (Apr 12 2021 at 21:27):Tadeusz Litak said:
I searched DuckDuckGo on moderate settings. I didn't even see a point in checking what happens if filters are completely off. "Rock cock" does sound worse than just "cock" to me.
People would look for "Rocq Coq" more, no?
Guillaume Claret (Apr 12 2021 at 21:30):I feel that whatever decision is taken, its implementation will be fine
Gabriel Scherer (Apr 20 2021 at 11:11):Is there a canonical place were we share our preferences about the names proposed in the wiki page? The idea is not (of course?) to start a voting process, it's just that I really like some of the proposals and I feel enthusiastic about saying it out loud. (But then maybe everyone here has had enough of the naming discussion already and you would rather welcome some other topic.)
Enrico Tassi (Apr 20 2021 at 12:27):You can formulate your thoughts here but the reasons why you like it better also be in the wiki.
Gabriel Scherer (Apr 20 2021 at 14:05):The wiki collects objective arguments but I think "Gabriel finds ... cute" has any worth on the list.
Gabriel Scherer (Apr 20 2021 at 14:07):One thing I considered doing is creating a "Weak proposals" category in which to move the proposals that have convincing arguments against (the bad ones!), for example Gallus, Chapon and Coquina.
Théo Zimmermann (Apr 20 2021 at 18:58):Yes, @Gabriel Scherer I think it makes sense to do that. It didn't when the page was very actively edited but now that's things are stabilizing, that would be useful.
Théo Zimmermann (Apr 20 2021 at 18:59):BTW, let me know if you'd be interested to take part in the WG that will be preparing the community survey.
Gaëtan Gilbert (May 21 2021 at 10:20):new proposals have slowed down, is it time for the next step?
Théo Zimmermann (May 21 2021 at 10:32):Agreed. Let's talk about this during the next Coq Call.
Théo Zimmermann (Jun 15 2021 at 17:04):Reading the comments at https://www.theregister.com/2021/06/15/coq_programming_language_change/, it looks like there is a joke to be made with the name "Coquand":
One commenter wrote:
So: Monsieur Coquand
BALLS
Another:
Argh
I was going to name my product Coquand. Balls.
Yet another:
If they rename to Coquand I'm definitely going top create a topology package named "Balls".
Can someone explain?
Guillaume Melquiond (Jun 15 2021 at 17:11):Not much to explain. If you replace "Coq" by "Coq &", then there is a bunch of words you can put afterwards, starting with "Balls".
Cyril Cohen (Jun 16 2021 at 10:10):Yep, basically they are mispronouncing Coquand's name...
Denis Bredelet (Jun 29 2021 at 22:46):I don't really have anything to do with Coq, but I was interested to see that people were considering changing the name, so it is good publicity!
Personally I like the proposal "Chantecleer"
My idea: Spoq
Andrey Klaus (Jul 02 2021 at 06:09):did somebody suggest just Galina already?
Andrey Klaus (Jul 02 2021 at 06:09):I would suggest Galina as name of all the system and the language
Théo Zimmermann (Jul 02 2021 at 06:32):Yes, this was one of the early proposal. See the wiki page.
Andrey Klaus (Jul 02 2021 at 09:28):have found and read it, thank you
Peter Sewell (Jul 22 2021 at 12:16):Just wondering how this is progressing? The more I have to talk about Coq-based projects, especially with industry folk from completely different communities, the more awkward I'm finding the historical name.
Théo Zimmermann (Jul 22 2021 at 12:28):Thanks for asking. We are still at the stage of triaging the proposals that were received to produce a shortlist. We expect to do the Coq community survey during the last quarter of 2021.
Peter Sewell (Jul 22 2021 at 12:42):Ack, thanks.
spaceloop (Dec 11 2023 at 09:46):What is the status of this plan? Is there any sort of timeline?
Huỳnh Trần Khanh (Dec 11 2023 at 11:57):yeah lol. can't wait to rename my pet project
Huỳnh Trần Khanh (Dec 11 2023 at 11:57):I'd say that the rename should be done soonish
Pierre Roux (Dec 11 2023 at 12:23):It's part of the forthcoming roadmap: https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md#change-of-name-coq---the-rocq-prover
spaceloop (Dec 11 2023 at 14:13):Thanks
Mike DuPont (Dec 12 2023 at 15:12):before i found this thread I already came up with a name https://github.com/meta-introspector/Alec
image.png
AINC Alec the Archaeopteryx is not Coq
Jason Rute (Dec 12 2023 at 16:38):Is there a recommended way to refer to Coq in current papers before the official rename? I guess if the new name isn’t certain, it probably is best to not mention it, right?
Jason Rute (Dec 12 2023 at 16:43):I wondering about something like the first place in the introduction were we say “This project use Coq, …” we say “This project uses Coq, to be renamed Rocq, …”.
Karl Palmskog (Dec 12 2023 at 16:45):there is no official announcement yet, so to my knowledge Coq should be called "Coq" until this happens
Paolo Giarrusso (Dec 12 2023 at 18:17):... also because the roadmap doesn't have an ETA on the legal checks and it can't predict their result. It's still cool progress, even if getting here already took so long.
Last updated: Oct 12 2024 at 12:01 UTC