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=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!goblin3!goblin1!goblin2!goblin.stu.neva.ru!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
Date: Tue, 9 Jul 2013 15:46:59 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <krhss4$6dr$1@loke.gir.dk>
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
 <krfb56$332$1@loke.gir.dk> <alpine.DEB.2.10.1307090935310.23845@debian>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: loke.gir.dk 1373402821 6587 69.95.181.76 (9 Jul 2013 20:47:01 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 9 Jul 2013 20:47:01 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
X-Original-Bytes: 2502
Xref: number.nntp.dca.giganews.com comp.lang.ada:182399
Date: 2013-07-09T15:46:59-05:00
List-Id: <comp.lang.ada>

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.10.1307090935310.23845@debian...
On Mon, 8 Jul 2013, Randy Brukardt wrote:

...
>> I don't know, nor care, because I don't see any reason or value to 
>> "Depends"
>> information in the first place.
>
>So you think, information flow analysis is completely worthless? (I mean,
>for building and verifying correct systems -- as a compiler writer you
>will not question the usage of information flow analysis inside the
>compiler or optimiser).

Information flow *within* a subprogram is important. Information flow 
*between* subprograms is completely defined by the subprogram's interfaces 
and calls. Other information ought to be irrelevant (no one should be 
depending upon what the body of Swap does, other than whatever is specified 
in the postcondition).

Janus/Ada does not do any inter-procedural optimizations, and I doubt that 
it would ever do any beyond inlining and parameter elimination -- neither of 
which have anything to do with flow analysis.

I realize that one can prove additional properties with this additional 
information, but my contention is that trying to do so is harmful (it adds a 
lot of coupling to a program) and isn't valuable to the vast majority of 
users. That is where Spark mostly went wrong, IMHO.

                Randy.