On Monday, 4 November 2013 at 20:26:18 UTC, Timon Gehr wrote:
On 11/04/2013 06:44 PM, qznc wrote:
On Saturday, 2 November 2013 at 13:59:53 UTC, Timon Gehr wrote:
It took decades to write a certified C compiler.
No, it took four years. CompCert was started in 2005.
CompCert is verified, not certified.
...
?
http://ncatlab.org/nlab/show/certified+programming
http://adam.chlipala.net/cpdt/html/Intro.html
Interesting definition. Seems not totally clear in the literature.
For me "certified" is always connected to some standard
documents. For example, the "Wind River Diab Compiler" [0] is
certified for DO-178B, IEC 60880, EN 50128, yada yada. This
certification is usually done by manual inspection and lots of
testing.
On the other hand, "verified" means (hopefully formal) proof.
CompCert itself [1] usually talks about "verification". As far as
I know, CompCert is not certified like the Wind River product
above. Hence, you are not allowed to use it in certain
high-safety applications (automotive,avionics,etc).
[0]
http://www.windriver.com/products/development_suite/wind_river_compiler/diab-details-4.html
[1] http://compcert.inria.fr/
