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.2 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,FROM_STARTS_WITH_NUMS autolearn=no autolearn_force=no
	version=3.4.4
X-Received: by 2002:a6b:8aa0:: with SMTP id
 c32-v6mr18445782ioj.85.1524764284951;
        Thu, 26 Apr 2018 10:38:04 -0700 (PDT)
X-Received: by 2002:a9d:5c8d:: with SMTP id a13-v6mr125249oti.0.1524764284760;
 Thu, 26 Apr 2018 10:38:04 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!feed.usenet.farm!feeder4.feed.usenet.farm!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!k65-v6no5669515ita.0!news-out.google.com!15-v6ni6633itg.0!nntp.google.com!f63-v6no5667511itc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 26 Apr 2018 10:38:04 -0700 (PDT)
In-Reply-To: <pbs316$ad8$2@gioia.aioe.org>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=85.243.127.167;
 posting-account=rhqvKAoAAABpikMmPHJSZh4400BboHwT
NNTP-Posting-Host: 85.243.127.167
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>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <d39f8a7e-1568-48a2-982d-f1ac6cecf975@googlegroups.com>
Subject: Re: How to get Ada to "cross the chasm"?
From: Mehdi Saada <00120260a@gmail.com>
Injection-Date: Thu, 26 Apr 2018 17:38:04 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 2585
X-Received-Body-CRC: 3287251363
Xref: reader02.eternal-september.org comp.lang.ada:51730
Date: 2018-04-26T10:38:04-07:00
List-Id: <comp.lang.ada>

Please bear with my ignorance, but from the exterior, it does seem that verification can switch on or off at a very fine level of granularity. At least in Spark 2014, with pragma spark_mode on/off.
I'm surprised to read that seniors/experts like Randy almost despise Spark. Can you provide more information ?
Do you find that:
1) the idea of proving formally is most of the time too much time consuming/almost not feasible for humans ?
2) good idea, but badly integrated with the language ?
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 ?

I suspect it's 3. Are there elaborated critics of the formal proof tendency somewhere on the web, NOT coming from C or some lazy/poorly typed language's people ?