status of Programming by Contract (PEP 316)?

[Russ]

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