It gets worse: a standard technique for proving correctness of imperative programs is called Hoare Logic, after C.A.R. Hoare, the inventor of Quicksort. And of course there is an implementation of Hoare logic in Coq.
I was asked a while back to give a talk about this stuff at work. It's maybe a relief that it didn't happen, since I dreaded having to say these names in today's environment. My plan was to put the slides up first (with the names and their origins on them), before saying the names out loud.
I don't think "coq" is slang for penis in French, though my French is at best rudimentary. I'm familiar with "verge" ("rod") and a few similar terms being used that way in French, but the English connotation of Coq's name is coincidental, I think.