Everyone who writes safety critical software should read this

[qznc]

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/