[tlringer]

We are mostly researchers, so this is not so much a language we use as our life's work. This means we talk about it a _lot_, including in public. It's not just about people at work making jokes; it's also about what happens when you leave work and mention what you do in public as a force of habit. It's pretty awful to expect all of us, especially the women in the community, to have to police the behavior of every stranger we encounter who hears us say that we are Coq experts or something similar, and uses that to make jokes at our expense or harass us.

[Rule35]

A guy I work with has 'balls' in his name. Yes, he and management expect people to keep their mouths shut.

Anyways, yes we could require him to change his name because it's distracting. That would be one thing to do. It's the solution suggested by people in this thread...

[tlringer]

If you can't see the many differences between those situations, I don't feel like we will have a productive conversation.

[Rule35]

Both involve expecting people to respect foreigners and their language.

There's a difference of magnitude, in that one is a guy's name and the other is a guy's project's name. But no, I don't see a fundamental difference.