3 ms·
Is Formal Specification used by proving language like Coq and Idris? Are they a different way of doing the same thing? Or two completely different thing?
by dorfsmay 8y ago
Is Formal Specification used by proving language like Coq and Idris?
Are they a different way of doing the same thing?
Or two completely different thing?
- pron 8y agoThey share many philosophical similarities, but their design and goals are very different. Coq 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.