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.