A few things I notice from skimming the paper and perusing related sites: 1. Although the source is available free of charge, CompCert is not free software. I

A few things I notice from skimming the paper and perusing related sites: 1. Although the source is available free of charge, CompCert is not free software. I couldn't find pricing on the AbsInt site or the North American vendor's site ("Ask for a quote"). 2. Currently targets IA32, 32-bit PowerPC, and ARMv6. 3. Covers most of C99, except VLAs and certain abuses of switch statements (e.g., Duff's device). 4. Faster and smaller code than GCC -O0, reasonably close to -O1 and -O2. John Regehr points out: "If we want better code out of [GCC et al.] we can turn on their optimizers, but at that point they would fail to be capable of translating 1,000,000 random programs without miscompiling a few times." http://blog.regehr.org/archives/1052 http://blog.regehr.org/archives/1052 I'm less inclined to use C as time goes by, but for the embedded market that CompCert targets, it seems like a really useful tool.