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.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!de-l.enfer-du-nord.net!feeder2.enfer-du-nord.net!feeder1.enfer-du-nord.net!gegeweb.org!news.ecp.fr!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Fri, 12 Jul 2013 15:07:23 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <7ebe0439-fa4c-4374-a6c7-365ac78e6e39@googlegroups.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373659643 21212 69.95.181.76 (12 Jul 2013 20:07:23 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 12 Jul 2013 20:07:23 +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: 2589 Xref: number.nntp.dca.giganews.com comp.lang.ada:182498 Date: 2013-07-12T15:07:23-05:00 List-Id: "Simon Wright" wrote in message news:lyd2qoutno.fsf@pushface.org... > "Randy Brukardt" 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.