Re: The future of Spark . Spark 2014 : a wreckage

["Randy Brukardt" <randy@rrsoftware.com>]

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