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

[Diez B. Roggisch]

Paul Rubin schrieb:
> "Diez B. Roggisch" <deets at nospam.web.de> writes:
>> For example, SPARK does not support dynamic allocation of memory so
>> things such as pointers and heap variables are not supported.
> 
> Right, Spark uses a profile intended for embedded systems, so
> no unpredictable gc delays etc.
> 
>> 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.
> 
> Yes, that's the usual approach.
> 
>> 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.
> 
> Whether the program uses dynamic memory allocation or not, there
> either has to be some maximum number of targets that it can be
> required to track, or else it's subject to out-of-memory errors.
> If a maximum number is specified, then memory requirements can
> be computed from that.

In other words: you pre-allocate everything and can then proove what - 
that the program is going to be stop working?

  What does that buy you - where is "I'm crashed becaus I ran out of 
memory trying to evade the seventh mig" better than "sorry, you will be 
shot down because I'm not capable of processing more enemie fighters - 
but hey, at least I'm still here to tell you!"

Sorry, but if that's supposed to make a point for static typechecking, I 
don't buy it. Crippling the execution model so that it fits a 
proving-scheme which essentially says "don't do anything complex  with 
me" is no good.

Diez