[nickpsecurity]

I reposted your link on Lobste.rs. I noted that COGENT already was doing verified functional with certified translation to C or assembly. Also that F star to C seems to be Microsoft and INRIA's route. So, at least two projects are making it much easier to verify algorithms or protocols in functional way with C code resulting.

The other thing I noted is that most code meant for verification is designed to be easy for humans or machines. The F star and C is one of few that is easy for both. I rarely see that.

[pjmlp]

On the talk that they did, the guy from F* team mentioned that their goal was to be able to validate that the C code is correct and they can match 1:1 the language constructs, to allow for proper verification of the generated code.