[tlringer]

> These re-namings always follow the same pattern. Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction.

Hello, I'm the woman who chimed in with the story of the Uber driver harassing me. I'm not just a Coq expert (check my publications), but also a contributor to the proof assistant (check my Github). Every year during non-pandemic times I go to France for a week for the Coq Users & Developers Workshop, and I am quite close with the team.

I also hear "Coq" before "cock" when people say either of those words, naturally, since I spend so much time working on Coq. Unfortunately, this means that in public I frequently forget that almost everyone who has never heard of it before hears "cock," and this is what most often gets me into bad situations like in the Uber.

The problem isn't that we are community outsiders; it's that you can't imagine us being community insiders.

[thu2111]

Surely the easier and better solution is to just give the driver a one star rating, rather than confusing anyone who has ever heard of coq and missed the re-naming. The costs you are inflicting on the software industry are very large when added up, for no good reason (people have to deal with dumb/ annoying taxi drivers all the time).

[tlringer]

If I were the only one complaining, I'd agree (with this being unnecessary---I don't quite see how the cost here is very large). But many women in the community both in the US and in France echo my experiences and concerns, as do many men. I also view it as part of my job as incoming faculty to discuss things that students may feel too vulnerable to discuss themselves.

Also, many on the core Coq development teams at Inria just feel this is bad branding for them at this point, as it inhibits adoption of the tool internationally.