[OT] F* for C crypto code

[leonardo]

A kind of nice talk about using F* language to verify crypto code that ends being compiled to C (some parts of it are in Firefox57):

Verified Low-Level Programming Embedded in F*

I hope we'll see some of this proved for Rust.