Re: SPARK - an idea for high integrity data structures

[Phil Thornley <phil.jpthornley@gmail.com>]

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