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!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: How to get Ada to "cross the chasm"?
Date: Sun, 29 Apr 2018 11:23:41 -0700
Organization: A noiseless patient Spider
Message-ID: <87o9i1oor6.fsf@nightsong.com>
References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com>
	<878t9nemrl.fsf@nightsong.com>
	<de23c005-4b50-4910-9327-6d4acdaa7270@googlegroups.com>
	<87h8o7lowg.fsf@nightsong.com>
	<c15bd651-b717-420e-a0d2-7ed27289cd28@googlegroups.com>
	<8736zqkwat.fsf@nightsong.com>
	<6839088c-f221-4650-a6ea-1841ae539486@googlegroups.com>
	<1e5f5681-0e2a-43cc-9437-2bd38078da08@googlegroups.com>
	<87604lvkqp.fsf@nightsong.com>
	<0bd80336-595a-45b6-b4e5-26c13d5859cb@googlegroups.com>
	<87o9idsh7f.fsf@nightsong.com>
	<b2ec5521-db67-40d8-8001-21853ab5222e@googlegroups.com>
	<87k1t1s9lx.fsf@nightsong.com> <pbr1e3$kfl$1@franka.jacob-sparre.dk>
	<pbs316$ad8$2@gioia.aioe.org>
	<d39f8a7e-1568-48a2-982d-f1ac6cecf975@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="2973c66b8467d5e5c38d149f2cdfa94b";
	logging-data="489"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19L9IH8rfLzyzH+swBIDH50"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:mjGdWTFn5rTqQiIhmPbjGVJaXWQ=
	sha1:zWPGXaKZAieITDelicAPTuvXWKA=
Xref: reader02.eternal-september.org comp.lang.ada:51804
Date: 2018-04-29T11:23:41-07:00
List-Id: <comp.lang.ada>

Mehdi Saada <00120260a@gmail.com> writes:
> At least in Spark 2014... Do you find that:
> 1) the idea of proving formally is most of the time too much time
> consuming/almost not feasible for humans ?

One thing I'd add is that automatic proving has gotten much better.
There's a page at Adacore (don't have the url offhand) mentioning some
Spark-83 program that had several hundred verification conditions (=
assertions needing to be proved).  SPADE was able to prove around half
of the VC's automatically, which meant the other half required
manually-written proofs.  With Spark-2014 and CVC3, the automatic
portion went up to around 90%.  

> 3) good idea, but the focus on it made designers lose focus on
> improving soundness of the language, so that the compiler would not
> need additional tools and efforts to achieve the same level of code
> quality ?

Well that's kind of philosophical, but I'd say the software world should
support a spectrum of approaches ranging from casual to extreme.  Casual
would mean something like Python or a spreadsheet.  Intermediate might
be something like Ada without SPARK.  Extreme requires proofs, or else
it wouldn't be extreme.

So should Ada support extreme approaches?  Or should it stay with
intermediate ones and leave the extreme ones to something else, and what
would the something else be?  I've always thought Ada aimed directly at
supporting the most rigorous approaches available, which means extreme
ones.  So to me, SPARK is part of what makes Ada interesting.