> 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. -- http://mail.python.org/mailman/listinfo/python-list
