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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Thu, 7 May 2015 11:12:16 +0200
Organization: cbb software GmbH
Message-ID: <1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net>
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> <mif9j3$ord$1@dont-email.me>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:25751
Date: 2015-05-07T11:12:16+02:00
List-Id: <comp.lang.ada>

On Thu, 07 May 2015 11:01:26 +0200, Georg Bauhaus wrote:

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

A compiler compiles, evidently...

The fallacy of Randy's conclusion is different. A compiler need not to be
the compiler from single language. The proof language is another language.
It cannot be same language because that is inconsistent. Yet it can and
must be compilable. It even can produce executable code, so long the
proof's code and the program's code are separate.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de