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.
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.
Comments
There is also the F* version, which can be made to target C via their KreMlin compiler.
https://project-everest.github.io/
https://fstarlang.github.io/general/2016/09/30/introducing-k...
Presented at this year's ICFP conference.
https://www.youtube.com/watch?v=sP7PRHn9iEA
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.
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.