One legend surrounding the name of the Coq programming language is that there was another theorem prover called Bit -- a word that, in French, sounds a lot like bitte. So the French researchers behind Coq, in ironic tribute, named their theorem prover with a French word that soumds like an English word for the human anatomy part that bitte describes.