3 ms·
They are many similarities and many differences, but the differences mostly stem from their goals being very different. Coq, Agda and Idris are mostly used for
by pron 8y ago
They are many similarities and many differences, but the differences mostly stem from their goals being very different. Coq, Agda and Idris are mostly used for research. TLA+ is designed for heavy-duty, everyday use in industry by software and hardware developers working on large, complex real-world systems.
- deleted 8y ago[deleted]
- hwj 8y agoAFAIK 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 8y 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