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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Thu, 07 May 2015 11:01:26 +0200
Organization: A noiseless patient Spider
Message-ID: <mif9j3$ord$1@dont-email.me>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
 <AnYlw.957256$Rp.242412@fx23.iad>
 <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
 <wccoaqucn51.fsf@shell01.TheWorld.com>
 <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
 <alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
 <wccegrpq2om.fsf@shell01.TheWorld.com>
 <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com>
 <ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
 <midvq5$2u3$1@loke.gir.dk>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 7 May 2015 09:00:19 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="7af0ebc34d55cbc312a7591190144f98";
	logging-data="25453"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18b4u4lfipZNLWnZFYHJDG/ElruY19Npk0="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:31.0) Gecko/20100101 Thunderbird/31.6.0
In-Reply-To: <midvq5$2u3$1@loke.gir.dk>
Cancel-Lock: sha1:BW/N+9Ifcu3lrV9ACoK2yyequ2M=
Xref: news.eternal-september.org comp.lang.ada:25750
Date: 2015-05-07T11:01:26+02:00
List-Id: <comp.lang.ada>

On 06.05.15 23:07, Randy Brukardt wrote:
> In order for proof to
> be part of the compiler, the proof language has to be part of the language.

If the proof language is understood by the compiler, this does not
require it to be compilable Ada, or efficiently computable (and
terminating in time), I think?

While a conjecture, say, can be rephrased as an Ada function,
the function may not be known to be got by a terminating computation.
Now what if a program's proof sill relies on this conjecture?

 From this point of view, proof things may either mean more than Ada
can express, or compute. That's not always handled by a global
assertion_policy.
Right now, the proof language (i.e. GNAT-SPARK) is using language extensions
that blend with Ada syntax. Earlier proof languages (such as e.g. SPARK)
used comments, and also understood (some) Ada.

That's not unusual: there are languages that have languages embedded
in string literals or in quoted expressions, used when formatting
or when interpolating or EVAL-ing, etc.