AFAIK Coq is used by CompCert[0], which is used for safety-critical software in ... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

hwj on April 15, 2019 | parent | context | favorite | on: Learn TLA+ (2018)

AFAIK Coq is used by CompCert[0], which is used for safety-critical software in the industry[1].

[0] http://compcert.inria.fr/ [1] https://www.absint.com/index.htm

pron on April 15, 2019 [–]

CompCert is written in Coq, and was developed as a research project at academic institutions [1]. It's a very small program (about 1/5 the size of jQuery) that has taken world-experts years to develop.

[1]: https://en.wikipedia.org/wiki/CompCert

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact