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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,a57260cce403bdae
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news1.google.com!news2.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail
From: Stephen Leake <stephen_leake@stephe-leake.org>
Newsgroups: comp.lang.ada
Subject: Re: SPARK GPL 2011 and SPARKSkein 2011
References: 
 <f7d3702b-1207-4c5d-8497-8a5130d6af20@v12g2000vby.googlegroups.com>
Date: Thu, 21 Jul 2011 04:42:04 -0400
Message-ID: <82hb6g58kj.fsf@stephe-leake.org>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (windows-nt)
Cancel-Lock: sha1:zQVHD6PcdUtD3DdRmyXl4v518es=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
X-Complaints-To: abuse@flashnewsgroups.com
Organization: FlashNewsgroups.com
X-Trace: 631764e27e673e029e66123202
Xref: g2news1.google.com comp.lang.ada:20261
Date: 2011-07-21T04:42:04-04:00
List-Id: <comp.lang.ada>

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