3 ms·
I know Coq as a tool to help generate proofs. Does it generate code? Either way, it's not a verified implementation of TLS. For that, we'd need: (1) A set of
by lallysingh 13y ago
I know Coq as a tool to help generate proofs. Does it generate code? Either way, it's not a verified implementation of TLS.
For that, we'd need:
(1) A set of properties to verify for an implementation
(2) An implementation to verify
Looking at http://coq.inria.fr/related-tools http://coq.inria.fr/related-tools, there may be some related tools that could do the job. Still, there's a research project there.
- dllthomas 13y agoPeople absolutely use Coq to generate code. I don't know what else is involved. A few substantiating links from my search results for "coq generating code": http://coq.inria.fr/V8.1/refman/Reference-Manual021.html http://coq.inria.fr/V8.1/refman/Reference-Manual021.html http://research.microsoft.com/en-us/um/people/akenn/coq/LOLA2012.pdf http://research.microsoft.com/en-us/um/people/akenn/coq/LOLA... http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...
- lallysingh 13y agoOh great! Thanks. Upvoted.