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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,640b65cbfbab7216
X-Google-Attributes: gid103376,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!y18g2000pre.googlegroups.com!not-for-mail
From: Eric Hughes <eric.eh9@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Ada.Strings.Bounded
Date: Tue, 15 Apr 2008 20:11:04 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <62273487-1b65-4434-9124-fc3b60d2cc94@y18g2000pre.googlegroups.com>
References: <q5CdnepU0ZzTxmzanZ2dnUVZ_t-nnZ2d@earthlink.com>
	<47F26C46.3010607@obry.net> <oYSdnZzY7_T8P2_anZ2dnUVZ_uGknZ2d@earthlink.com>
	<44d88b93-6a90-4c18-8785-2164934ba700@a9g2000prl.googlegroups.com>
	<47F652F7.9050502@obry.net>
 <d478eba3-b8d5-4727-bdd6-2fd68c341427@n1g2000prb.googlegroups.com>
	<e29ab2eb-4d08-4f15-96b4-de8318a94bab@1g2000prg.googlegroups.com>
	<47f7028d$1_6@news.bluewin.ch> <47F749CB.30806@obry.net>
 <f10fbaff-0546-4c3f-9d62-267bbdcea7ea@w4g2000prd.googlegroups.com>
	<728033b9-52c1-4951-ba22-5067467dad50@b5g2000pri.googlegroups.com>
	<90d313e2-115b-4998-ad2d-3d0c4d84f841@q24g2000prf.googlegroups.com>
	<48039eb1$0$629$9b4e6d93@newsspool1.arcor-online.net>
 <8862aecc-c70d-46cc-a140-f26d9b0acfb4@z24g2000prf.googlegroups.com>
	<4805111d$0$636$9b4e6d93@newsspool1.arcor-online.net>
NNTP-Posting-Host: 166.70.57.218
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1208315464 14991 127.0.0.1 (16 Apr 2008 03:11:04
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 16 Apr 2008 03:11:04 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: y18g2000pre.googlegroups.com; posting-host=166.70.57.218;
	posting-account=5RIiTwoAAACt_Eu87gmPAJMoMTeMz-rn
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US;
 rv:1.8.1.13)
	Gecko/20080311 Firefox/2.0.0.13,gzip(gfe),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:20970
Date: 2008-04-15T20:11:04-07:00
List-Id: <comp.lang.ada>

Eric Hughes wrote:
> This is where that Hoare
> paper that I mentioned a while back, "Proof of correctness of data
> representations" comes in.  It describes exactly how this works.

On Apr 15, 2:33 pm, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> Thanks for the title. I see that some methods are actually
> heading in this direction. Hopefully, the basic idea that
> data and timing must be formally correct, too, finds its way
> into education.

You're welcome.  That essay is collected in the book _Essays in
Computing Science_.

The title of that essay might well have been titled "Proof of
correctness of compiler output", but Hoare doesn't go into compilation
issues as such in enough depth to justify such a title.  You'd have a
program annotated with some properties and their proof, a compiler
that converted the proof to one in its execution model, and proof-
carrying object code as its output.  Even if the proof annotations of
the program were empty (as today), you can still infer some basic
semantics from expressions and statements by themselves and generate
checkable proof.  I suspect that discipline would get rid of a lot of
code generation defects.

Eric