4 ms·
Am waiting for Coq developers to start showing up and asking for Rust projects to be rewritten using Coq / Compcert.
by dman 9y ago
Am waiting for Coq developers to start showing up and asking for Rust projects to be rewritten using Coq / Compcert.
- snakeanus 9y agoSadly Compcert is not foss, meaning that they will have a huge problem if they try to push it everywhere. I think that the age of non-free languages and implementations meant for the general public is over, even MS has made their C# and F# implementations free.
- Jweb_Guru 9y agoCompcert is guaranteed to compile correct C code to correct assembly (given its TCB assumptions). It doesn't say anything about incorrect C code. So in order to benefit from CompCert, first you have to prove that you have valid C in the first place, which is no easy feat. You'd probably be better off using a language that's designed with verification in mind, like Cogent or ADA/Spark, or waiting for lambda-Rust to become production ready, since in those cases you won't have to prove tedious bureaucratic memory safety invariants for the vast majority of your code, and can focus on functional correctness (or, if you just care about memory safety, you can stop there).