F* – An ML-like functional programming language aimed at program verification

Re:F* – An ML-like functional programming language aimed at ... by qualitytime on Monday October 30, 2017 @04:40AM (#15583711)

"Current status - We generate a C library, but the verification is not complete."

[ Parent | on HN ]

Re:F* – An ML-like functional programming language aimed at ... by catalin_hritcu on Monday October 30, 2017 @06:27AM (#15584048)

One can always look at the empty part of the glass, but the quote does continue with a big full part:

"The TLS 1.3 handshake verification is work in progress and still relies on the OCaml extraction mechanism of F* ; thus, the C library still encapsulates the OCaml runtime system.

We have completed verification of the TLS 1.3 record layer it currently extracts to C.

The AES and SHA2 cryptographic assembly routines are verified and extract to assembly via Vale.

HaCl* provides verified C code for multiple other primitives such as Curve25519, Chacha20, Poly1305 or HMAC.

Our test client implements TLS 1.2 + TLS 1.3 Draft 18 and successfully connects to TLS 1.3 test servers. We have a prototype integration of miTLS within libcurl that one can use to git clone a remote repository."

[ Parent | on HN ]

Re:F* – An ML-like functional programming language aimed at ... by tom_mellior on Monday October 30, 2017 @05:38AM (#15583882)

Note however that the page does list a bunch of useful, completely[1] verified components just below that sentence.

[1] Modulo things like the correctness of their C semantics, assembly semantics, various extraction procedures.

[ Parent | on HN ]

Re:F* – An ML-like functional programming language aimed at ... by sitkack on Tuesday October 31, 2017 @10:33AM (#15593501)

Vs the pile that is OpenSSL.

[ Parent | on HN ]