status of Programming by Contract (PEP 316)?

[Russ]

Ricardo Aráoz wrote:

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

I don't quite see it that way.

I would agree that if your OS and compiler are unreliable, then it
doesn't make much sense to bend over backwards worrying about the
reliability of your
application. But for real safety-critical applications, you have no
excuse for not using a
highly reliable OS and compiler. For really critical stuff, I think
the real-time OSs are usually
stripped down to
the bare basics. And if you are using something like SPARK Ada, the
language itself is
stripped of many of the fancier features in Ada itself. (There's also
something called the
Ada Ravenscar profile, which I believe is geared for safety-critical
use but is not quite as
restrictive as SPARK.)

Keep in mind that the OS and compiler are typically also
used for many other applications, so they tend to get tested fairly
thoroughly. And remember
also that you won't have extraneous applications running -- like a web
browser
or a video game, so the OS will probably not be heavily stressed. The
most likely source
of failure is likely to be your application, so bending over backwards
to get it right makes
sense.

Then again, if you are running C on Windows, you might as well just
give up on reliability
from the start. You don't have a prayer.