2 ms·
AFAIK Coq is used by CompCert[0], which is used for safety-critical software in the industry[1]. [0] http://compcert.inria.fr/ http://compcert.inria.fr/ [1] ht
by hwj 7y ago
AFAIK Coq is used by CompCert[0], which is used for safety-critical software in the industry[1].
[0] http://compcert.inria.fr/ http://compcert.inria.fr/
[1] https://www.absint.com/index.htm https://www.absint.com/index.htm
- pron 7y agoCompCert 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 https://en.wikipedia.org/wiki/CompCert