Generating C code that people want to use

Using KreMLin, a dedicated compiler, the verified F* code is compiled to readable C, meaning existing systems projects can readily integrate our verified code. In short, even if it doesn’t matter for a C compiler, the expectation was truly that the resulting C code would be as crisp, clean and readable as what a C programmer would have written. It took us a long way to get there, but we are now ready to scale up to multiple consumers of our code, an excellent news as we gear up towards more software releases, such as EverCrypt, which I shall cover in a later blog post.

Source: jonathan.protzenko.fr