From: Simon Wright <simon@pushface.org>
Subject: Re: SPARK - an idea for high integrity data structures
Date: Tue, 20 Jul 2010 20:18:49 +0100
Date: 2010-07-20T20:18:49+01:00 [thread overview]
Message-ID: <m2lj96t10m.fsf@pushface.org> (raw)
In-Reply-To: 4c45f3e7$0$2388$4d3efbfe@news.sover.net
"Peter C. Chapin" <pcc482719@gmail.com> writes:
> I know Praxis is working on generics support in SPARK. Once that was
> ready it probably wouldn't be too hard for the original author of a
> high integrity collections library to generalize the code as
> appropriate. At least that would be my hope.
An alternative might be to use an external macro processor to generate
appropriate code complete with annotations. I guess that would depend on
whether the proofs (a) didn't depend on the contained type, (b) didn't
need (much) human intervention.
next prev parent reply other threads:[~2010-07-20 19:18 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-07-20 12:40 SPARK - an idea for high integrity data structures Phil Thornley
2010-07-20 14:33 ` Matteo Bordin
2010-07-20 19:02 ` Phil Thornley
2010-07-20 19:07 ` Peter C. Chapin
2010-07-20 19:18 ` Simon Wright [this message]
2010-07-21 12:40 ` Phil Thornley
2010-07-21 13:23 ` Peter C. Chapin
2010-07-22 10:14 ` Matteo Bordin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox