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,6941f5cd4f1d4739
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!u26g2000yqu.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK - an idea for high integrity data structures
Date: Tue, 20 Jul 2010 12:02:17 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <3c05d4bd-b796-4ff0-a36f-24a3550d4749@u26g2000yqu.googlegroups.com>
References: 
 <9ac8feb3-5b79-41b1-a124-df211039c1bc@c10g2000yqi.googlegroups.com>
	<1a490b86-e9cf-46c4-8f2e-3d633b51fa50@y13g2000yqa.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1279652537 11595 127.0.0.1 (20 Jul 2010 19:02:17
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 20 Jul 2010 19:02:17 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: u26g2000yqu.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:12484
Date: 2010-07-20T12:02:17-07:00
List-Id: <comp.lang.ada>

On 20 July, 15:33, Matteo Bordin <matteo.bor...@gmail.com> wrote:

> you may be interested in having a look at Hi-Lite:
>
> http://www.open-do.org/projects/hi-lite/
>
> and in particular this discussion:
>
> http://lists.forge.open-do.org/pipermail/hi-lite-discuss/2010-June/00...

Thanks for that - a very relevant discussion! However I did notice
this in one of the contributions:
"Our major focus is to make user proofs easy. Whether or not we prove
the implementations of such containers is to be decided latter and not
our current focus."

But my main interest is in proving the implementations so fortunately
I'm not directly duplicating this work.

Cheers,

Phil