Walter Bright wrote:
> retard wrote:
>> The contract programming only covers a small runtime dynamic part of
>> programming. There's no mention about automated theorem proving. No
>> word about exceptions nor sandboxing with virtual machines. Why?
>> Because these would make D look ridiculous.
>
> That misses the point about reliability. Again, you're approaching from
> the point of view that you can make a program that cannot fail (i.e.
> prove it correct). That view is WRONG WRONG WRONG and you must NEVER
> NEVER NEVER rely on such for something important, like say your life.
> Software can (and will) fail even if you proved it correct, for example,
> what if a memory cell fails and flips a bit? Cosmic rays flip a bit?
>
Plus, how do you prove the proof? I know of at least two examples
of software that were proven formally and that AFAIK worked
perfectly to spec and yet failed spectacularly. One of them caused a
Mars probe to crash (it had been proven using measurements in feet,
but the sensors were reporting in kilometers IIRC) and the other
caused the ground control crew to activate the self destruct for the
first Ariane 5 rocket (it had been proven using data designed for
Ariane 4 and no longer valid for Ariane 5).
Jerome
--
mailto:jeber...@free.fr
http://jeberger.free.fr
Jabber: jeber...@jabber.fr
signature.asc
Description: OpenPGP digital signature
