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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: How to get nice with GNAT?
Date: Tue, 25 Nov 2014 20:18:21 +0100
Organization: A noiseless patient Spider
Message-ID: <m52kld$s8g$1@dont-email.me>
References: <slrnm6u97f.nrc.lithiumcat@nat.rebma.instinctive.eu>
 <dda292cb-97ac-4ab5-b29d-b3c0ec232c5b@googlegroups.com>
 <m4th8h$jce$1@dont-email.me>
 <0d8452a9-68c9-4835-b6f3-17407132ca9f@googlegroups.com>
 <jtq67a5ffb7fm44joao6a7nbvav7mdq29o@4ax.com>
 <8194a204-7b15-463d-a2fd-4d3ba342fe97@googlegroups.com>
 <8f203a9a-6c7c-4614-bc7d-efa65bf10776@googlegroups.com>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 25 Nov 2014 19:18:06 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="28944"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19Jy1wN3kzPUewS0q2LaTmgzj2cu9LAo/M="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:24.0) Gecko/20100101 Thunderbird/24.6.0
In-Reply-To: <8f203a9a-6c7c-4614-bc7d-efa65bf10776@googlegroups.com>
Cancel-Lock: sha1:CH6Yy3k94M41XdQAAhcYran9uw4=
Xref: news.eternal-september.org comp.lang.ada:23717
Date: 2014-11-25T20:18:21+01:00
List-Id: <comp.lang.ada>

On 25.11.14 16:07, ake.ragnar.dahlgren@gmail.com wrote:
> Of course I always listen seriously to Jeff Carter but it's not obvious to me that doing "C in Ada" is bad. If I remember correctly Google employees are recommended to avoid using exceptions when doing C++. The designers of Google Go has gone great lengths to avoid the exception concept as much as possible. In addition SPARK forbids usage of exceptions.

Tucker Taft, designer of both Ada 95 and ParaSail has not
put Ada's exceptions in his ParaSail language(*). The latter
language does presume a lot of checking at compile time, though,
of logical expressions etc.; all of this is almost entirely absent
from C programs.

That's not without consequences for a fair comparison.

Some static analyzers re-interpret the C language by adding
rules and information that is not present in either C programs
or in the C language. The interpretation may likely be what
the programmers would have intended, but still inference cannot
magically add all of the same logical information to a C program
that would be present in a ParaSail program. Moreover, a program's
meaning then begins to essentially depend on the QoI of a compiler,
not on the language or on your own expressions as a program's author.

As these and previous efforts both at language design and
at compiler technology will influence AdaCore, it seems likely
that Ada 2012's contracts can both reduce the need for checks
at run-time and add assurance based on real expressions,
while also improving diagnostic messages if provers look at
the assertions, the calls, and the implementations.

There are the beginnings specific mentions of exception
identifiers in post-conditions, IIUC.

    Post => that_will_be_true(...) or else raise  ...;

ParaSail...
"eliminates run-time exception handling -- strong compile-time
  checking of preconditions and support for parallel event-handling
  provides a safer alternative;"

__
(*)https://forge.open-do.org/plugins/moinmoin/parasail/