I’ve started learning a theorem proving tool to help me with my thesis. It’s called Coq, which has got to be the most unfortunate name I can think of. I think the creators are French, and coq means cock, as in rooster, in French. Why rooster? I have no idea. Why does anyone name anything what they do? I wonder which seemingly-innocent English words mean something equally awkward in other languages?