Re: Reference-oriented language and high-integrity software

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

Maciej Sobczak <no.spam@no.spam.com> writes:
>> 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.
>
> This can be rebutted on the basis that those languages ensure that
> nothing like this happens (no pointer arithmetic + garbage collector).

And your rebuttal can be rebutted at the highest criticality levels
where you do not certify the source text, but the object code emitted
by the compiler.  In those contexts you do not even trust the
compiler.  References make the object code even more difficult to
certify.

>>  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
>
> This makes sense in case of Java, but one could also argued that
> immutability of objects - a common feature in some reference-oriented
> languages - can make it less severe.

Yes, provided you trust the compiler - which you don't in
high-integrity software.

> So - let's imagine a language, which is reference-oriented with all
> objects immutable. Apart from dynamic memory, is there any problem?

Yes.  Tracing the object code to the source text, and certifying the
object code.  I'm not saying it's impossible to do; just that it's
unacceptably expensive to do.

-- 
Ludovic Brenta.