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,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.107.149.140 with SMTP id x134mr1031518iod.65.1511032155316;
        Sat, 18 Nov 2017 11:09:15 -0800 (PST)
X-Received: by 10.157.89.211 with SMTP id u19mr289968otg.14.1511032155175;
 Sat, 18 Nov 2017 11:09:15 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.kjsl.com!usenet.stanford.edu!i6no551542itb.0!news-out.google.com!193ni1158iti.0!nntp.google.com!d140no541923itd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sat, 18 Nov 2017 11:09:14 -0800 (PST)
In-Reply-To: <00d9e86b-c1be-49a9-a8e3-b0cec114c859@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=89.15.184.193;
 posting-account=vDt8RwoAAADiHfuXLUrBu4GU_iEKvtUX
NNTP-Posting-Host: 89.15.184.193
References: <d8eab147-bf05-4f6d-b333-b65c9c99cb69@googlegroups.com>
 <00d9e86b-c1be-49a9-a8e3-b0cec114c859@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <53eb97c3-bb17-4e66-8286-35ce8b97230d@googlegroups.com>
Subject: Re: ANN: article on Ada language for audio applications
From: Gustavo Hoffmann <gusthoff.ada@gmail.com>
Injection-Date: Sat, 18 Nov 2017 19:09:15 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: feeder.eternal-september.org comp.lang.ada:48993
Date: 2017-11-18T11:09:14-08:00
List-Id: <comp.lang.ada>

Thanks!

> Have you considered to go further to formal proof with SPARK?
> 

Yes, I have considered that. Unfortunately, due to time-constraints, I was not able to work on it. In general, formal proof of numerical algorithms is an interesting topic.

Gustavo.