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

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

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyd2qoutno.fsf@pushface.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> GNAT has a pragma Pure_Function which can be used on a single
>> function. This isn't in Ada because it is just an assumption; there is
>> no checks at all whether it is true. In that case, any mistake in the
>> function would make a program calling it erroneous (because the
>> compiler is allowed to assume the function is pure, even if it
>> isn't). It can only be made safe if it is combined with a proof that
>> there are no side-effects, in which case it surely should never be
>> separated from that proof -- but pragmas are *always* separated from
>> the thing they apply to. As such, they are never appropriate for
>> setting properties of single entities.
>
> GNAT supports Pure_Function as an aspect; so you can write
>
>   package Pf is
>      function F (X : Integer) return Integer with Pure_Function;
>   end Pf;

Right, but the semantics are still (arguably) wrong. We (the ARG) eventually 
concluded that Ada can't use the name Pure_Function because we didn't want 
to interfere with the existing GNAT implementation, and doing it without any 
checking at all is just a non-starter.

                                      Randy.