From: Stephen Leake <stephen_leake@stephe-leake.org>
Subject: Re: SPARK GPL 2011 and SPARKSkein 2011
Date: Thu, 21 Jul 2011 04:42:04 -0400
Date: 2011-07-21T04:42:04-04:00 [thread overview]
Message-ID: <82hb6g58kj.fsf@stephe-leake.org> (raw)
In-Reply-To: f7d3702b-1207-4c5d-8497-8a5130d6af20@v12g2000vby.googlegroups.com
Rod Chapman <roderick.chapman@googlemail.com> writes:
> SPARK GPL 2011 is now up on libre.adacore.com.
>
> We've also updated the SPARKSkein release to meet
> v1.3 of the Skein specification, and reproduced all
> analyses and proofs with the GPL 2011 toolset.
> This is at www.skein-hash.info.
Very interesting!
However, I think www.skein-hash.info could use a bit more propaganda
about what SPARKskein is, and why people should care about it.
For example, here is the abstract from the paper about SPARKskein:
(http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf)
This paper describes SPARKSkein – a new reference implementation of
the Skein algorithm, written and verified using the SPARK language
and toolset. This paper is aimed at readers familiar with the Skein
algorithm and its existing reference implementation, but who might
not be familiar with SPARK. The new implementation is readable,
completely portable to a wide-variety of machines of differing
word-sizes and endian-ness, and “formal” in that it is subject to a
proof of type safety. This proof also identified a subtle bug in the
implementation which persists in the C version of the code. The new
code offers similar performance to the existing reference
implementation. As a further result of this work, we have identified
several opportunities to improve both the SPARK tools and GCC.
Just getting this on the web page somewhere (perhaps on
http://www.skein-hash.info/downloads) would be very good. _Especially_
the parts about being completely portable (I'm assuming the C version is
not?), finding a bug in the C version, and "similar performance".
This is an excellent opportunity to advertise the benefits of Ada and
SPARK.
Hmm. That info is available at
http://www.altran-praxis.com/news/SPARKskein_16_Aug_10.aspx, which is
probably a more appropriate place for such things. Pardon my enthusiasm :)
Any update on the 'future work' section of the paper (improvements for
gnat, spark)?
--
-- Stephe
prev parent reply other threads:[~2011-07-21 8:42 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-07-20 12:39 SPARK GPL 2011 and SPARKSkein 2011 Rod Chapman
2011-07-21 8:42 ` Stephen Leake [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox