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.

While it is impressive work, is anybody using it in production?

On Sunday, 3 November 2013 at 03:03:58 UTC, Walter Bright wrote:
>
> Nobody pretends that the Space Shuttle flight control computers are safe. There are 4 of them, plus a 5th with completely different design & software in it. This is coupled with a voting system.

I heard they're retooling that system after the last design fell victim to the "hanging chad" problem.

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

On 11/4/2013 12:09 PM, Sean Kelly wrote:
> On Sunday, 3 November 2013 at 03:03:58 UTC, Walter Bright wrote:
>>
>> Nobody pretends that the Space Shuttle flight control computers are safe.
>> There are 4 of them, plus a 5th with completely different design & software in
>> it. This is coupled with a voting system.
>
> I heard they're retooling that system after the last design fell victim to the
> "hanging chad" problem.

?

On Monday, 4 November 2013 at 21:00:25 UTC, Walter Bright wrote:
> On 11/4/2013 12:09 PM, Sean Kelly wrote:
>>
>> I heard they're retooling that system after the last design fell victim to the "hanging chad" problem.
>
> ?

Jokes are so much less funny when you have to explain them.  Voting.  Hanging chads.  Sigh.

On 11/4/2013 3:44 PM, Sean Kelly wrote:
> On Monday, 4 November 2013 at 21:00:25 UTC, Walter Bright wrote:
>> On 11/4/2013 12:09 PM, Sean Kelly wrote:
>>>
>>> I heard they're retooling that system after the last design fell victim to
>>> the "hanging chad" problem.
>>
>> ?
>
> Jokes are so much less funny when you have to explain them. Voting.  Hanging
> chads.  Sigh.

Ah :-)

On Saturday, 2 November 2013 at 04:03:46 UTC, Walter Bright wrote:
> On 11/1/2013 8:03 AM, bearophile wrote:
> I think you're missing the point. Improving the quality of the software is not the answer to making fail safe systems.

Well, OTOH, worsening the software won't really increase the reliability of the system.

On Monday, 4 November 2013 at 20:09:27 UTC, Sean Kelly wrote:
> On Sunday, 3 November 2013 at 03:03:58 UTC, Walter Bright wrote:

> I heard they're retooling that system after the last design fell victim to the "hanging chad" problem.

I loved this one. And I learnt a thing:

http://www.answers.com/topic/what-is-a-hanging-chad

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/

On Tuesday, 5 November 2013 at 08:41:17 UTC, eles wrote:
> On Saturday, 2 November 2013 at 04:03:46 UTC, Walter Bright wrote:
>> On 11/1/2013 8:03 AM, bearophile wrote:
>> I think you're missing the point. Improving the quality of the software is not the answer to making fail safe systems.
>
> Well, OTOH, worsening the software won't really increase the reliability of the system.

Fail safe design needs to be engineered to handle the situation when any component fails regardless of the quality of components used. Software is just one more (weak) component in the system.

Of course component quality is important to overall safety because fail safe systems are not foolproof. But as Walter says it should not be part of the solution nor relied upon in a fail safe deign.