I wonder if it's more due to the strength of sexual taboos in America or the frequency of the word -- bits are referred to from the very beginning of the curric

I wonder if it's more due to the strength of sexual taboos in America or the frequency of the word -- bits are referred to from the very beginning of the curriculum, whereas theorem provers are only mentioned a few times unless you take a specific class. Both, perhaps - we are still a bit puritanical. After a lot of exposure, I map "coq" in a CS context to the theorem prover and don't find it giggle-worthy, but the reaction of students hearing it for the first time is different. (And outside of that, I'm more likely to think coq au vin, but I'm a cook.)