Howdy! Holger Levsen <holger at layer-acht.org> skribis: > I've heard about http://compcert.inria.fr/compcert-C.html and > http://compcert.inria.fr/ yesterday and I believe it is related… Unfortunately, CompCert is non-free. :-/ Also, it depends on Coq, which depends on OCaml, which is not “bootstrappable”. Ludo’.