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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Introductory Presentations, especially aimed at C++ programmers! Date: Thu, 8 Dec 2016 09:38:06 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <1905815374.502825168.454102.laguest-archeia.com@nntp.aioe.org> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32674 Date: 2016-12-08T09:38:06+01:00 List-Id: On 08/12/2016 09:08, Maciej Sobczak wrote: > The problem is - you did not provide any evidence to claim that > those same humans would not make such errors in Ada. > > SPARK is a game-changer in this area - but there are too few > long-lived internet-oriented open-source projects in SPARK to make a > realistic comparison either. That is, if for whatever reason it is > unrealistic to write such projects in SPARK, then SPARK is not a > solution, either. That's right. Exception contracts are long overdue and the design of proofs must allow mixed strategies instead of all-or-nothing. In most cases it would be enough to statically prove absence of exceptions. However, in the given case the proof must be about "no exception when registry key value is less than N" That goes more towards a full correctness proof. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de