-
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.
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
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!