Talia Ringer (Apr 12 2021 at 22:04): Talia Ringer (Apr 12 2021 at 22:04):If any of the other [besides anyone I've spoken to already] core Coq developers are upset with the way I phrased anything in the email thread, please feel free to let me know, that was not my intention
Emilio Jesús Gallego Arias (Apr 12 2021 at 22:29):I didn't see anything wrong Talia , do you write that for anything specific?
In the general discussion there was a very "ugly" thing [not from you] , regarding how a few participants:
Example of this are the original mail, which IMHO is in pretty poor form, or this https://news.ycombinator.com/item?id=26743882 , etc... I can understand some of French colleagues are less than pleased :/
I guess this is a defining characteristic of the XXI century , we are all entitled to express what we think, even if we know little about the matter at hand.
Emilio Jesús Gallego Arias (Apr 12 2021 at 22:31):Also I may be a bit "old school" in terms of communication, but it is not my way to handle issues with colleagues by public scandal
Emilio Jesús Gallego Arias (Apr 12 2021 at 22:31):I prefer to phone them and get more information about it, for example, if I see a problem with a logo, I'd first talk to the author of such logo, etc...
Another issue is that many people misunderstood what the problem with the name is, curiously very few of them (none) seem to be native speakers.
Marc Hermes (Apr 14 2021 at 11:41):Yishuai Li said:
I'm looking forward to a brand new version of the system called, say, CIC "CIC Isn't Coq".
Or instead use CIC as the new name, meaning "CIC is Coq".
Also it can be read as "sick" and I would be looking forward to hearing people talk about the "sick proof assistant".
Jonathan Sterling (Apr 15 2021 at 12:33):Emilio Jesús Gallego Arias said:
I didn't see anything wrong Talia , do you write that for anything specific?
In the general discussion there was a very "ugly" thing [not from you] , regarding how a few participants:
- assumed bad faith / intent from Coq devs a few times
- they dared to question information given by actual students of Huet, or just invent their own version of the history with little resemblance to reality and of course without even knowing the name of the original Inria team, or who and when actually created the logo, etc...
Example of this are the original mail, which IMHO is in pretty poor form, or this https://news.ycombinator.com/item?id=26743882 , etc... I can understand some of French colleagues are less than pleased :/
I guess this is a defining characteristic of the XXI century , we are all entitled to express what we think, even if we know little about the matter at hand.
If my understanding that the original naming of Coq was meant as a double entendre is in fact wrong, I will happily retract it. But this is what I have been told by multiple workers at Inria. (Btw if you want to talk to me, you can 'mention' me rather than just obliquely linking to something and insinuating that it is a lie.)
By the way, I think the original email _was_ bad because its wording very clearly implied that someone had intentionally made the logo look phallic --- whereas (unlike with the name) I don't think I have ever seen any reason to suspect that this was intentional. And I also felt the whole thing was gone about in not an ideal way, because it ignores the subtleties of how Coq is funded and the fact that the Coq developers and community are not the only stakeholders. It would be a shame if something like this were to spark a sequence of events that led to Coq losing funding, people in the Coq team losing their jobs due to unsubstantiated allegations, etc.
I think that it would have been better to deal with this in private with the Coq team, who have shown that they will work in good faith to address the concerns of the community. With all this said, I don't regret that the discussion happened; it is good that there is openness to changing the name, and the logo too I suppose.
Théo Zimmermann (Apr 15 2021 at 12:39):I think the fact that the discussion happened in public was not a bad thing actually. The naming question has been discussed many times in private before. This public discussion sparkled many testimonies which were really instructive, that we wouldn't have gotten otherwise.
Théo Zimmermann (Apr 15 2021 at 12:39):In particular, the ones about students refusing to learn Coq.
Théo Zimmermann (Apr 15 2021 at 12:40):But yes, the title of the discussion was terrible since it implied bad intent.
Jonathan Sterling (Apr 15 2021 at 12:40):Yes, I agree about the name discussion; I think the logo thing should have been done in private.
Théo Zimmermann (Apr 15 2021 at 12:41):As for the double entendre in the name, nobody is contesting that. But I think it is fair to make a distinction between "name chosen to troll" and "name chosen for other reasons but not discarded despite known issue in English".
Théo Zimmermann (Apr 15 2021 at 12:42):In particular, I think Hugo's answer to your HN comment summarizes it well.
Jonathan Sterling (Apr 15 2021 at 12:42):Perhaps we are having a language barrier issue... But to me, double entendres are meant to troll people who see the second meaning.
By the way, it would not be a double entendre if it just happened to have an offensive name in English and this was not part of the motivation for choosing the name. My understanding was that it _was_ considered, and this was part of the motivation for the name (it would be fun to hit back against US cultural imperialism or whatever). So if all that is true, then I stand by my comment. If not, then I would retract it.
Théo Zimmermann (Apr 15 2021 at 12:44):Well, I wasn't there so it's hard for me to give a definite answer but I still distinguish between "one of the reason for choosing the name" and "an accidental bonus" (I cringe while writing bonus). My understanding is that it was the latter.
Jonathan Sterling (Apr 15 2021 at 12:45):Hugo, whom I respect deeply, seems to have the misconception that the only way for it to be trolling is if the _only_ motivation were to troll. Based on what people have told me, it sounded like it was "one of the reasons" --- which, in the historical context described above in this thread, makes perfect sense.
Jonathan Sterling (Apr 15 2021 at 12:46):Anyway, there is enough of a gray area here that I hope you can see why I interpret the facts the way I do. And I sincerely do not appreciate @Emilio Jesús Gallego Arias's absurd characterization of my comments as contributing to some "ugliness", especially seeing as we generally are in agreement on almost the entire issue. It's just not appropriate.
Théo Winterhalter (Apr 15 2021 at 12:47):Given the tradition of picking an animal for a tool/language, I think it might have been named "coq" regardless, considering how well a fit it was.
Jonathan Sterling (Apr 15 2021 at 12:47):I don't personally know how long that tradition goes back ;-) a lot of the other ones were inspired by Coq.
Théo Winterhalter (Apr 15 2021 at 12:49):Right, I don't know either. :)
I personally started working on Coq long before hearing about this "extra" (not to say "bonus") justification for the name. I can't attest to the original intent, as most of us.
Jonathan Sterling (Apr 15 2021 at 12:50):I also want to be clear that I don't put too much blame on Huet, another scientist whom I have a lot of respect for even though I have some specific incidents that I am not happy with. It was a different time, and the project was very very small, and nobody could have predicted what an immense thing it would turn into. I think one also couldn't have predicted that it would become something that is used quite a lot in the English-speaking world, and I think that there wouldn't have been something wrong with having an "inside joke" among French people that is meant to push back against the tide of fashionable political correctness.
I think it is just a fact that this was one of the motivations of the name, and that while it would have been fine if Coq had been confined to France, today there is a responsibility to a much larger community that should be taken in to account. Which I am very happy to see that the Coq team are doing in such an admirable and open-minded way.
Bas Spitters (Apr 15 2021 at 12:50):@Jonathan Sterling The story also used to be in SF.
Coq was implemented in Caml :camel:
Emilio Jesús Gallego Arias (Apr 15 2021 at 12:52):Hi @Jonathan Sterling , sorry I didn't cite you here, I was not even aware if you had an account here, and I didn't think it would require a lot of discussion. Regarding my characterization of the comment
To be clear, this name was chosen by the creator of Coq, Gerard Huet, with the intention of trolling. It wasn't an innocent French word.
I have to stand by it. IMHO it is an incorrect characterization of intent, and as it was said by Hugo, it is not the reason the name was chosen. If "Coq" would have sound in english as "rock", the tool would still be named Coq.
Both for the logo and the name, quite exact characterization of their history have been given by a member of the team that was actually there, and the way I see it, they remain questioned, which is what I think seems strange.
Emilio Jesús Gallego Arias (Apr 15 2021 at 12:53):Bas Spitters said:
Jonathan Sterling The story also used to be in SF.
Coq was implemented in Caml :camel:
Actually first versions of Coq were not implemented in Caml, but in some forms of lisp [the reference manual has the complete history]
Théo Zimmermann (Apr 15 2021 at 12:54):Also, consider the impact of comments that make it look like the main reason for this name was to troll English speakers. And what image it gives to people who do not have the full story in mind...
Emilio Jesús Gallego Arias (Apr 15 2021 at 12:54):Théo Zimmermann said:
Also, consider the impact of comments that make it look like the main reason for this name was to troll English speakers. And what image it gives to people who do not have the full story in mind...
That's exactly my point.
Emilio Jesús Gallego Arias (Apr 15 2021 at 12:55):Or in the same discussion people asking Hugo to provide citations... He is the citation!
Jonathan Sterling (Apr 15 2021 at 12:55):I was mainly considering the impact of absurd comments that are saying that it's a total coincidence and just English PC-worshippers who are making a big deal out of nothing.
Jonathan Sterling (Apr 15 2021 at 12:56):It is not a coincidence, it was known from the start. Now my opinion is that I don't think it was necessarily bad for them to name it this way in the beginning. But I was not happy with some gas-lighting that I was seeing (I don't think necessarily coming from the coq team).
With all that said, I see what you mean about the conclusions that one could draw from my comment. For instance, Hugo drew a totally erroneous conclusion from my comment --- if someone like Hugo can draw such an erroneous conclusion, then surely the general public could as well. For this reason I would be very pleased to clarify my comment on that thread to prevent any damage.
Jonathan Sterling (Apr 15 2021 at 13:00):I have issued this clarification here in light of this conversation: https://news.ycombinator.com/item?id=26819899
I wish to clarify this comment; what I said above is strictly correct, but several people have drawn an undesirable conclusion from it which leads me to find a clarification necessary. It is not the case that trolling English speakers was the primary motivation of Huet. My understanding is that the trolling was a side-benefit to a name he would have chosen regardless of whether it evinced the double entendre.
Théo Zimmermann (Apr 15 2021 at 13:00):Thanks!
Emilio Jesús Gallego Arias (Apr 15 2021 at 13:07):Indeed that is correct; as I wrote on twitter people [especially outside of Inria] need to understand that this is a delicate matter and the level of formality on the professional level inside Inria.
If anyone writes "Coq was chosen to troll" or "the logo as made to look like a penis", this is first, incorrect, and second, puts researchers and the project itself into jeopardy as it is clear both of the above are not things that, if true, would be let go by the Inria direction.
I agree with Théo it is good for the discussions to happen in public, however I think those not having a first-hand understanding of the history behind the name / logo should exercise caution on drawing conclusions.
Tadeusz Litak (Apr 16 2021 at 16:05):Many French professors of Huet's generation were willing to demonstrate their dissatisfaction with the dominance of American culture and language (today's English is really AmEnglish, increasingly so even in the UK itself). But it does seem that over decades and subsequent retelling, for many people this factor grew to shadow everything else, and has led to dismissing all other factors and reasons as fake history. I have myself appreciated fully neither Huet's genuine willingness to honour Coquand at the time of switching to a new implementation (with CoC becoming an increasingly obsolete name) nor the sheer marketing brilliance of this particular name in France. Paradoxically, over last 10 days I started to appreciate the name more than I used to. Incidentally, I also did not appreciate the depth and richness of French rooster symbolism. For starters, it does not seem to pit the nation with its complex history into pro-Marianne vs. pro-Joan-of-Arc camps.
Tadeusz Litak (Apr 16 2021 at 17:13):Even in the coq-club discussion itself (in which Jonathan did not participate, for all I see), the original motivation was quickly reduced to trolling and a bad joke. On the first day, Jennifer Paykin correctly pointed out that the issue of this original intention is orthogonal to the question of, e.g., students being discouraged by the name; similar observations supported by personal testimonies have been made later by Kristin, Stephanie, Wilayat or Marie. On the second day, Théo and Emilio added important voices from the developers' team; sadly, a bit late and at a stage when sensible voices were increasingly lost in the noise. By then, the avalanche was in full speed.
Tadeusz Litak (Apr 16 2021 at 17:43):It didn't help that the author of the original post was so proud of its title and form that he dumped it on twitter as well (I don't have a twitter account, which makes twitter particularly easy to read). In general, the effect of so-called academic twitter (a contradiction in terms, if you ask me) not just on brains and emotional state of some researchers, but on the well-being of the entire community is something for a separate discussion, which sooner or later must be had and which is going to be much more painful than the present one. Ditto for the addiction of too many students and researchers to the hysteria of American or British politics, mass media, and slogan chanting.
gallais (Apr 16 2021 at 17:55):This is getting off topic & the characterization of people who just described their experiences as "[not] sensible voices" and "hysteria" is ridiculous. This last adjective in particular carries a lot of history and when the topic is centered around hearing women's voices it seems like a very strange choice of words.
Tadeusz Litak (Apr 16 2021 at 18:07):In the coq-club discussion too, there were more than enough people who contributed neither a personal perspective, nor a fresh point of view, nor a constructive proposal, but piled in just for the sheer glory of grandstanding. What I found particularly grating were absolutist phrases ("trumping all other considerations", "any barrier has no right to be endorsed by an official organization"), slogan chanting such as "we should strive to do better, and we can do better" and terms like "victimhood", "suffering" and "oppression". This is a complex and subtle discussion of branding, for crying out loud, not the second Paris Commune or liberation of Buchenwald. Seems some people simply do not even know anymore how to use a different language and how to think in a more precise way.
Tadeusz Litak (Apr 16 2021 at 18:13):gallais said:
This is getting off topic & the characterization of people who just described their experiences as "[not] sensible voices" and "hysteria" is ridiculous. This last adjective in particular carries a lot of history and when the topic is centered around hearing women's voices it seems like a very strange choice of words.
You are deliberately misrepresenting the actual content of my comment, in more ways than one.
No, I am very explicitly not talking about those who just described their experiences. In fact, these are precisely the voices I counted as sensible ones.
The kind of language that is used in your post is precisely what I am talking about though. I can't help if you feel offended by this.
gallais (Apr 17 2021 at 07:38):You can't at the same time say "Seems some people simply do not even know anymore how to use a different language and how to think in a more precise way" and also complain that you using a word with a massive history of misogyny attached to it is irrelevant to the conversation and a misrepresentation of your position.
Anyway, I won't feed your trolling any more than that. The core team accepts and understands the problem. That's the main issue.
Tadeusz Litak (Apr 17 2021 at 12:49):gallais said:
You can't at the same time say "Seems some people simply do not even know anymore how to use a different language and how to think in a more precise way" and also complain that you using a word with a massive history of misogyny attached to it is irrelevant to the conversation and a misrepresentation of your position. Anyway, I won't feed your trolling any more than that.
Théo Zimmermann (Apr 17 2021 at 15:28):The fact you feel offended by this may say more about you...
@Tadeusz Litak Personal attacks are not welcome on this forum or anywhere in Coq's community (https://github.com/coq/coq/blob/master/CODE_OF_CONDUCT.md) and this part of your statement above really looks like one. The fact that Guillaume didn't interpret your comment correctly doesn't make you legitimate to answer like that. (You could argue that he misrepresented your comment while avoiding personal attacks.) I suggest that you take a break from posting new comments in this thread for a while. If you think that my intervention is inadequate, still do take some time to calm down before answering.
Last updated: Oct 13 2024 at 01:02 UTC