status of Programming by Contract (PEP 316)?

[Ricardo Aráoz]

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.
> 
> 

In that case why don't we just 'certify to a higher level' the programs
and get done with this formal proofs? We should remember that the level
of security of a 'System' is the same as the level of security of it's
weakest component, so either we formally prove all those other very
important components (OS gets MUCH more use than the program (the
program uses it for almost every other action)) or get done with the
whole fuss.