3 ms·
(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 t
by 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.