Comment on F*: A general-purpose proof-oriented programming languageComments−LelouBil1moI like Haskell, and to me this seems really useful as a kind of "noob" to functional languages.Is this used in the industry ? And for what kind of software ?−nextaccountic1moFirefox cryptographic primitives are written and formally verified in F*Some Windows things too I think (I think F* is partially funded by Microsoft Research)They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementationshttps://project-everest.github.io/https://github.com/hacl-star/hacl-starhttps://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)−LelouBil1moI found these links in the F* bookhttps://www.microsoft.com/en-us/research/blog/everparse-hard...https://lwn.net/Articles/770750/https://project-everest.github.io/
Comments
I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages.
Is this used in the industry ? And for what kind of software ?
Firefox cryptographic primitives are written and formally verified in F*
Some Windows things too I think (I think F* is partially funded by Microsoft Research)
They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementations
https://project-everest.github.io/
https://github.com/hacl-star/hacl-star
https://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)
I found these links in the F* book
https://www.microsoft.com/en-us/research/blog/everparse-hard...
https://lwn.net/Articles/770750/
https://project-everest.github.io/