6 ms·
I remember reading (and I don't have a source for this so this is total hearsay) that basically when Coq/CoC was chosen, it was chosen with the awareness of the
by rtpg 5y ago
I remember reading (and I don't have a source for this so this is total hearsay) that basically when Coq/CoC was chosen, it was chosen with the awareness of the "sounds like cock lol" factor being a plus.
This is far from the first "french mathematicians with a 10-year-old's sense of humor" thing, and probably won't be the last, but all this "oh it's just a word in French" is, from my undrestanding, bait.
To be honest, I'm not super convinced the process discussed the article is happening in much good faith either. But that's just my opinion and heavily biased towards my own experiences interacting with people from Inria.