PEP 3107 and stronger typing (note: probably a newbie question)

[Diez B. Roggisch]

John Nagle schrieb:
> Chris Mellon wrote:
>> You can't prove a program to be correct, in the sense that it's proven
>> to do what it's supposed to do and only what it's supposed to do.
> 
>     Actually, you can prove quite a bit about programs with the right 
> tools.
> For example, proving that a program cannot subscript out of range is
> quite feasible.  (Although not for C, where it's most needed; that language
> is just too ill-defined.) 

You can - when there is input involved?

> You can prove that certain assertions about
> an object always hold when control is outside the object.  You can
> prove that certain entry conditions for a function are satisfied by
> all its callers.
> 
>     Take a look at what the "Spec#" group at Microsoft is doing.
> There's also some interesting USAF work on avionics at
> 
> http://www.stsc.hill.af.mil/crossTalk/2006/09/0609SwardGerkenCasey.html

"""
For example, SPARK does not support dynamic allocation of memory so 
things such as pointers and heap variables are not supported.
"""

Pardon me, but if that's the restrictions one has to impose to his 
programs to make them verifiable, I'm not convinced that this is a way 
to go for python - or any other language - that needs programs beyond 
the most trivial tasks.

Which is not to say that trivial code couldn't have errors, and if it's 
extremely cruical code, it's important that it hasn't errors. But all I 
can see is that you can create trustable, simple sub-systems in such a 
language. And by building upon them, you can ensure that at least these 
won't fail.

But to stick with the example: if the path-planning of the UAV that 
involves tracking a not before-known number of enemy aircrafts steers 
the UAV into the ground, no proven-not-to-fail radius calculation will 
help you.

Diez