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!news3.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 02:58:36 -0600 From: Ludovic Brenta Newsgroups: comp.lang.ada Subject: Re: Reference-oriented language and high-integrity software References: Date: Fri, 03 Nov 2006 09:58:51 +0100 Message-ID: <87mz78zz1w.fsf@ludovic-brenta.org> User-Agent: Gnus/5.110006 (No Gnus v0.6) Emacs/21.4 (gnu/linux) Cancel-Lock: sha1:V5HamrA4KxSkpswInYnqGpUqd5E= MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii NNTP-Posting-Host: 62.235.207.236 X-Trace: sv3-iOzZEmss5yyCc+QYnB1MjyWcWXQQDeLCUsbzFW9j0u2BqWgpJSBBCRGirBpELPlLvm0SQphuYv3iQbP!7HkeKX/ZcN3N8qtlm+ambkVUtB9rEikMgWTMsW1o5p6kEm2kfHiGCELiwLiG1NeGKzac4j1OCj4= 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:7347 Date: 2006-11-03T09:58:51+01:00 List-Id: Maciej Sobczak 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.