Functional Programming in Coq

• coq

  24 4,428 9.6 OCaml

  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.

  

  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...

• hn-search

  459 500 0.0 TypeScript

  Hacker News Search

  

  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

• Onboard AI

  getonboard.dev

  sponsored

  Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.

  

Suggest a related project