Re: Reference-oriented language and high-integrity software

[Georg Bauhaus <bauhaus@futureapps.de>]

Ludovic Brenta wrote:
> Maciej Sobczak <no.spam@no.spam.com> writes:

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

On what premises?
I could argue that an index value, while being in
range of its subtype, points(!) to the wrong half of an array.
While this looks like an algorithmical issue, 
deterministic handling of preallocated storage can be an algorithmic
issue, too. What about placement new or storage pools?
How expensive is proving an algorithm that maps a finite number
of source text variables to a fixed size storage pool as a function
of <...experts insert here...>?