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

[Paul Rubin]

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