The problem with Coq
-
There's a famous tool for theorem proving which is called "Coq", after the French name for rooster and also after it's name inventor, whose first name is Coquand.
They've become sick of the countless jokes that resulted from that name, so they are thinking of a better one. There's some bullshit "diversity, equity, inclusion" arguments, too, of course.
https://github.com/coq/coq/wiki/Alternative-names
https://www.theregister.com/2021/06/15/coq_programming_language_change/Turns out that one of the main problem is that basically every word is in some language a slang word for penis.
-
@klaus said in The problem with Coq:
Turns out that one of the main problem is that basically every word is in some language a slang word for penis.
You're pulling my Klaus, as they say in Wales.
