What does HackerNews think of 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.
Language:
OCaml
Which category does Coq go in?
With code example:
https://github.com/coq-community/coq-100-theorems/blob/maste...
here are a few
- https://github.com/mirage/mirage
- https://github.com/returntocorp/semgrep
- https://github.com/bcpierce00/unison
See https://v2.ocaml.org/learn/companies.html for some more leads, as lots of those companies maintain useful OSS software.
The same can be done also with Coq[1], it is easy to learn[2], actively developed[3], and better documented[4]. You can also visit their discussion board[5]. Regarding the usual Lean vs Coq "war" and so-called "setoid hell" you can read a lengthy discussion on their GitHub[6].
[2] https://learnxinyminutes.com/docs/coq/
[3] https://github.com/coq/coq
[4] https://softwarefoundations.cis.upenn.edu/
I wonder if it somehow can be integrated with Coq[1] and Univalent Foundations[2]. Probably these can be used as a more substantial "base" for this machine.