| You beat me to it. Unlike the other commenters, I see that you're describing it as a robust, predictable start to what Bernstein describes. Undefined behavior and other problems can be caught by extensions to the compiler or via static analysis tools like an Astree Analyzer knockoff. The fact that they'll be written in Ocaml (or SML) will make them more reliable. A good choice and what I've promoted here so far. Additionally, the clean passes are easier to bootstrap for those that fear subversion of their compiler. Can use whatever you want on whatever machine to implement it. So long as code matches spec, the output should be the same. That implementation compiles the other compilers, verifiers, whatever. You might also enjoy that people have already extended CompCert work and others for developments that push in the Boring, Safe/Secure, C compiler direction. Here's some: CakeML - Compile CompCert, etc with this
https://cakeml.org/ Verasco - verified, CompCert-based, static analyzer for C
http://compcert.inria.fr/verasco/ Verification of LLVM transformations later work (eg Softbound or Code-pointer Integrity clone)
http://repository.upenn.edu/dissertations/AAI3592852/ Extension of CompCert for verified, WCET analysis
https://hal.inria.fr/hal-01087194 So, lots of good stuff being done by a subset that focus on right design methods with the right tools. And they're getting incredible results. Surprise! :) |