Re: Reference-oriented language and high-integrity software

[Ludovic Brenta <ludovic@ludovic-brenta.org>]

Maciej Sobczak <no.spam@no.spam.com> writes:
> Taking into account that JB also wrote a book about SPARK, some
> reasoning can be found there and my understanding (simplified) is that
> reference-oriented language implies a heavy use of dynamic memory,
> which makes it impractical/impossible to perform any static analysis
> of memory consumption. Garbage collectors add their own factors to the
> problem.
>
> Is the above a reasonable explanation? Is it the only one? What else
> makes the reference-oriented languages inappropriate for
> high-integrity software?

The other part of the explanation, AFAIU, is that a reference can go
wrong, i.e. point to deallocated memory, to unallocated memory, or to
the wrong piece of memory.  References also introduce aliasing,
i.e. two references can point to the same item.  All these make it
almost impossible to statically prove that no unintended side effects
ever occur in the program (correctness means: do what you're supposed
to do; safety means: do not do what you're not supposed to do.  It is
this latter part that matters to the present discussion).

-- 
Ludovic Brenta.