Formal specification and proof (was : Does Python really follow its philosophy of "Readability counts"?)

[Ricardo Aráoz]

Mark Wooding wrote:
> Steven D'Aprano <steve at REMOVE-THIS-cybersource.com.au> writes:
>
>   
>
>> No it's not. It's *practical*. There are domains where *by law* code
>> needs to meet all sorts of strict standards to prove safety and
>> security, and Python *simply cannot meet those standards*.
>>     
>
> Codswallop.  One can prove stuff about Python programs using the same
> techniques as one uses for any other language.  I've done it.  Other
> languages have better automated tools, it's true -- but the techniques
> are basically the same.
>
>   
I've seen this kind of thinking and there are a couple of things about
which I've always wondered.
Let's say you formally specify an application (hey! you are a
zillionaire and can afford it), and that after the app is coded you
formally prove that it complies with the specification. Cool! now your
app is safe? NO, because your formal proof was done over source code and
the compiler has not been formally specified and proven. So your app
might still fail. So let's say you have the $ to do that and you get a
perfect compiler. Are you safe? NO, because the code generated by the
compiler makes calls to the OS which is not specified. So let's assume
you are a world leader and you spend a little war's money in fully
specifying and proving an OS. Are you safe? NO, because the processor
and other hardware logic has NOT been specified. And on and on.

What I've seen engineers do when they need extra safety is to put in
place independently developed and operated redundant systems, at least
three, and the system will do whatever two of the independent systems
agree on. So I guess if I really wanted to be safe with a system I'd
have it made by at least three different teams (yes, also the
requirements should be written by different teams) in different
languages under different OS's and different independent machines. And
THEN I would have some measure of safety (and this would certainly be
more cost effective than the formal specification route).


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-list/attachments/20090122/ec1c08e6/attachment-0001.html>