(Potentially-relevant fact: I am a woman.)

I first heard of Coq in a CS lecture, and it wasn’t at all off-putting. The professor included the obligatory “yes the name sounds funny” disclaimer and then presented an interesting walkthrough of Coq. I haven’t used Coq myself yet, but that has more to do with the difficulty of starting than the name. I’ve enjoyed the Natural Number Game (a web-based set of Lean exercises), as a good example of something which actually helps people get into theorem proving. This debate over the name of Coq is just an instance of the Law of Triviality.

While you may not have felt that way, other women have. Does your experience invalidate theirs?

No, I’m just providing my own n=1.

(Why is it that “I am unhappy” is justified to report, but “I am alright” isn’t? Don’t we want a representative sample of opinions?)

It's perfectly fine, and in mature settings it should be a non-issue. But I've learnt to be wary of assuming everyone is fine with it, or assuming that everyone will behave. I mean, tech bros will tech bro. I'm not in favour of helping them perform deniable harassment.

This is harmless banter and anyone not resilient enough to handle this will face much greater distress during their working life. Adults should be able to handle childish humor and this movement towards infantilizing women seems a much greater issue to me. All this will achieve is giving power to political narcissist.

Interesting, how you’re so set on the name of a theorem proving software being the barrier to women entering the field and not the people who would actually harass them. Do you not think the same people who would make stupid jokes about a name wouldn’t find some other way to chase women away?

I'm just listening to what women say. You should try it sometime.

https://twitter.com/sydgibs/status/1379518799699968005

The name lends itself for innuendos, so what? I can assure you that a person with sleazy intentions will find many ways to do that without a funnily named programming language. The name is not the problem. Also, a person's offense is not an argument. I'm offended by your name, do you have to change it now? A funnily named programming language just isn't the same as actual sexual harassment.

Women are not children, they understand and appreciate humour. You being offended on behalf of them frankly seems more insulting. This kind of hyper-sensitive attitude is what drives women away from CS, not the word "coq".

Well, it's actually women in CS being offended, and I'm merely engaging with the blockheads who refuse to acknowledge the issue.

Are there real people offended by it? Or just three Twitter users?

Quite an accusation from a sockpuppet account that has been completely dormant since 2017.

Ah yes, sockpuppet. The term people use when they have good arguments.

Look at the account, it's a classic phony, stashed away for sniping without new account green.

Do you really think I played such a long game? In any case the other commenter is right -- you shouldn't attack the person, but the argument itself.

No smart theorem proving woman has ever been turned down by Coq. I know this because they would need to be familiar with Coq in the first place. Or would they have trained on Prolog instead?

Your statement doesn't follow any logic.