status of Programming by Contract (PEP 316)?

[Steve Holden]

Russ wrote:
>> I've always wondered... Are the compilers (or interpreters), which take
>> these programs to machine code, also formally proven correct?
> 
> No, they are not formally proven correct (too complicated for that),
> but I believe they are certified to a higher level than your "typical"
> compiler. I think that Ada compilers used for certain safety-critical
> applications must meet higher standards than, say, GNU Ada, for
> example.
> 
> And the OS
>> in which those programs operate, are they also formally proven correct?
> 
> Same as above, if I am not mistaken.
> 
>> And the hardware, microprocessor, electric supply, etc. are they also
>> 'proven correct'?
> 
> I think the microprocessors used for flight control, for example, are
> certified to a higher level than standard microprocessors.
> 
> How would you prove a power supply to be "correct"? I'm sure they meet
> higher reliability standards too.
> 
>
"... I believe ...", "... if I am not mistaken", "I think ...".

Well, all this certainty you are expressing will surely allow this bozo 
to sleep more soundly in his bed.

Frankly I am getting a little tired of they way you are unable to even 
recognize that your readers may well have a sensible appreciation of the 
difficulties about which you write. As has been pointed out already, 
many readers here are extremely experienced programmers.

You said in an earlier post "that's not an insult", but that isn't 
really up to you to decide. If it gives offense then it probably is, 
whether it was intended to do so or not. You don't seem to appreciate 
the insulting nature of your tone, and calling people bozos is not 
likely to endear you to most c.l.py readers since it comes off as arrogant.

Given that you now profess no absolute certainty on fairly simple 
matters connected to safety-critical systems I wish you'd step down off 
your platform and join the rest of us.

regards
  Steve
-- 
Steve Holden        +1 571 484 6266   +1 800 494 3119
Holden Web LLC/Ltd           http://www.holdenweb.com
Skype: holdenweb      http://del.icio.us/steve.holden
--------------- Asciimercial ------------------
Get on the web: Blog, lens and tag the Internet
Many services currently offer free registration
----------- Thank You for Reading -------------