From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,25e091afe1184988
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news4.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local01.nntp.dca.giganews.com!nntp.scarlet.biz!news.scarlet.biz.POSTED!not-for-mail
NNTP-Posting-Date: Fri, 03 Nov 2006 05:15:29 -0600
From: Ludovic Brenta <ludovic@ludovic-brenta.org>
Newsgroups: comp.lang.ada
Subject: Re: Reference-oriented language and high-integrity software
References: <eiet3r$2on$1@cernne03.cern.ch>
	<87mz78zz1w.fsf@ludovic-brenta.org> <eif0qu$4k8$1@cernne03.cern.ch>
Date: Fri, 03 Nov 2006 12:15:44 +0100
Message-ID: <87hcxgye5b.fsf@ludovic-brenta.org>
User-Agent: Gnus/5.110006 (No Gnus v0.6) Emacs/21.4 (gnu/linux)
Cancel-Lock: sha1:lPnj5xUo28vgZRL+KFHkefNK+Q0=
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
NNTP-Posting-Host: 62.235.207.236
X-Trace: 
 sv3-sOrzzLBUAAZ+h1/mP/T3DBqACiGNJGaHy2d4+Y88l5sU7ZREpSi4qMEbIhrS5k7TrRcRxNGT5nE/KhR!VTqmAoM3Uvt2yo7ah4i8QVVot6fFNP9Jls9Bhu7X83I3PR2nUT2h7bZ5j7NdVRT6ymiyAlk/mKQ=
X-Complaints-To: abuse@scarlet.be
X-DMCA-Complaints-To: abuse@scarlet.biz
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.32
Xref: g2news2.google.com comp.lang.ada:7351
Date: 2006-11-03T12:15:44+01:00
List-Id: <comp.lang.ada>

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.