status of Programming by Contract (PEP 316)?

[Ricardo Aráoz]

Neil Cerutti wrote:
> On 2007-08-31, Ricardo Aráoz <ricaraoz at gmail.com> wrote:
>> Russ wrote:
>>> Yes, thanks for reminding me about that. With SPARK Ada, it is
>>> possible for some real (non-trivial) applications to formally
>>> (i.e., mathematically) *prove* correctness by static analysis.
>>> I doubt that is possible without "static declarative type-
>>> checking."
>>>
>>> SPARK Ada is for applications that really *must* be correct or
>>> people could die.
>> I've always wondered... Are the compilers (or interpreters),
>> which take these programs to machine code, also formally proven
>> correct? And the OS in which those programs operate, are they
>> also formally proven correct? And the hardware, microprocessor,
>> electric supply, etc. are they also 'proven correct'?
> 
> Who watches the watchmen? The contracts are composed by the
> programmers writing the code. Is it likely that the same person
> who wrote a buggy function will know the right contract?
> 

Actually my point was that if a program is to be trusted in a critical
situation (critical as in catastrophe if it goes wrong) then the OS, the
 compiler/interpreter etc should abide by the same rules. That is
obviously not possible, so there's not much case in making the time
investment necessary for correctness proof of a little program (or
usually a little function inside a program) when the possibilities for
failure are all around it and even in the code that will run that
function. And we should resort to other more sensible answers to the
safety problem.