Our great sponsors
-
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
What ever happened to the effort [1] to rename Coq in order to make it less offensive? There were a number of excellent proposals [2] that seemed to die on the vine.
[1] https://github.com/coq/coq/wiki/Alternative-names
[2] https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3...
The linked proposal is about the reactions of people unfamiliar with the concept. There are 133 comments on HN which contain both "coq" and "cock"[0]. At the least, there's a lot of comments about changing the name (as well as a HN discussion explicitly about renaming Coq from two years ago[1]).
[0] https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
[1] https://news.ycombinator.com/item?id=26738980
Related posts
- Change of Name: Coq –> The Rocq Prover
- Why Mathematical Proof Is a Social Compact
- Mark Petruska has requested 250000 Algos for the development of a Coq-avm library for AVM version 8
- How are people like Andrew Wiles and Grigori Perelman able to work on popular problems for years without others/the research community discovering the same breakthroughs? Is it just luck?
- Where does it all start!