6 ms·
Why? To appease puritans? I‘d rather have them release a library for coq named tits (after the birds of course).
by emsy 5y ago
Why? To appease puritans? I‘d rather have them release a library for coq named tits (after the birds of course).
- angry_octet 5y agoYou can keep have genitalia discussions down at the pub, see how many women want to listen to you talk Coq. We don't need Coq double entendres in the workplace, but we do need smart women in the theorem proving community.
- thewakalix 5y ago(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.
- angry_octet 5y agoWhile you may not have felt that way, other women have. Does your experience invalidate theirs?
- thewakalix 5y agoNo, 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?)
- angry_octet 5y agoIt'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.
- emsy 5y agoThis 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.
- swat535 5y agoWomen 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".
- angry_octet 5y agoWell, it's actually women in CS being offended, and I'm merely engaging with the blockheads who refuse to acknowledge the issue.
- AlexeyBelov 5y agoAre there real people offended by it? Or just three Twitter users?
- angry_octet 5y agoQuite an accusation from a sockpuppet account that has been completely dormant since 2017.
- emsy 5y agoAh yes, sockpuppet. The term people use when they have good arguments.
- angry_octet 5y agoLook at the account, it's a classic phony, stashed away for sniping without new account green.
- AlexeyBelov 5y agoDo 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.
- Bancakes 5y agoNo 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?
- angry_octet 5y agoYour statement doesn't follow any logic.
- the_only_law 5y agoInteresting, 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?
- angry_octet 5y agoI'm just listening to what women say. You should try it sometime. https://twitter.com/sydgibs/status/1379518799699968005 https://twitter.com/sydgibs/status/1379518799699968005
- emsy 5y agoThe 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.
- inigojonesguy 5y agoTits alternative is a great theorem in mathematics. https://en.wikipedia.org/wiki/Tits_alternative https://en.wikipedia.org/wiki/Tits_alternative
- deleted 5y ago[deleted]