status of Programming by Contract (PEP 316)?

[Ricardo Aráoz]

Russ wrote:
> Paul Rubin wrote:
>> Bruno Desthuilliers <bdesth.quelquechose at free.quelquepart.fr> writes:
>>> FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained"
>>> why one can not hope to "write reliable programs" without strict
>>> static declarative type-checking.
>> I don't know about Eiffel but at least an important subset of SPARK
>> Ada's DBC stuff is done using static analysis tools (not actually
>> built into the compiler as it happens) to verify statically
>> (i.e. without actually running the code) that the code fulfills the
>> DBC conditions.  I don't see any way to do that with Python
>> decorators.
> 
> 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'?

> With all
> due respect, most (not all, but most) Python programmers never get
> near such programs
> and have no idea about how stringent the requirements are. Nor do most
> programmers
> in general, for that matter. (It's not an insult)
>