status of Programming by Contract (PEP 316)?

[Neil Cerutti]

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?

-- 
Neil Cerutti
The third verse of Blessed Assurance will be sung without musical
accomplishment. --Church Bulletin Blooper