Hacker News new | ask | show | jobs
by fargle 64 days ago
why did they find the need to rename this? Am i missing something?
3 comments

The linked community survey suggests that a plurality of votes were in favour, which would explain it: https://discourse.rocq-prover.org/t/coq-community-survey-202...
The name sounded like Cock.
Because U.S. English is everything, and people want it that way, and any concern about cultural imperialism that would immediately be brought up in any other context magically doesn’t apply when Americans could possibly be offended. Everyone else has to adapt, no matter their mother tongue.

Meanwhile the world’s most common VCS’s name is literally an abuse (not a misspelling of one), but only outside the US so nobody cares.

Practically speaking there's no reason not to centralize on the particulars of one language while the rest are in the increasingly accelerated process of dying out. Language barriers help nobody. Though it is a shame to rename this, the world needs more whimsy and penises are funny.