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

Preferably something generated from a formal proof tool. It wouldn't be perfect (nothing is), but the mistakes would be less stupid. Which is a big jump!

There's a bit of research in this, but I don't know of anything that's ready to use.




Well, there's Coq, which (per my understanding) may or may not make the cut depending on how you define "ready to use".


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, there may be some related tools that could do the job. Still, there's a research project there.


People 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://research.microsoft.com/en-us/um/people/akenn/coq/LOLA...

http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...


Oh great! Thanks. Upvoted.


Maybe ADA SPARK?:

http://senier.net/libsparkcrypto/




Consider applying for YC's Spring batch! Applications are open till Feb 11.

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

Search: