Why? To appease puritans? I‘d rather have them release a library for coq named tits (after the birds of course).
We don't need Coq double entendres in the workplace, but we do need smart women in the theorem proving community.
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.
(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?)