Re: Pure function aspect?...

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

<stefan-lucks@see-the.signature> wrote in message 
news:Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de...
> On Thu, 12 Jan 2012, Randy Brukardt wrote:
...
> However, another reason, why the AI became so complex, seems to be the
> attempt to rather precisely specify side-effects, instead of providing
> just the ability to declare "no side effects".

There has been strong opposition to a "checked" pure function declaration (I 
had floated that first, and it went nowhere), and global in out => null is 
essentially the same thing. The reason is the "memo function" idea (more 
sensibly, a function that logs its calls but is otherwise pure) is not 
allowed. I was trying to do something broader that could get more support.

And just declaring "no side-effects" without checking it is actively harmful 
in my opinion because, perversely, it makes a program less safe. That's 
because the compiler is going to take advantage of this declaration to 
remove calls (especially in contracts and assertions), and if the call in 
fact has side-effects, doing that is not safe (and can easily lead to bugs 
or even erroneous execution). (And if you aren't going to let the compiler 
take advantage of this knowledge, declaring it is pointless.)

I have some lengthy examples of this problem that are tooo long to present 
here (and at least get any other work done), but trust me, it is very real.

The lack in global in out isn't a deal breaker for Ada 2012, simply because 
it is also missing exception contracts. And we need (at least) both of those 
to have enough completeness to really reason formally about Ada programs. 
Hopefully, future versions of Ada will take up both of these again.

                                          Randy.