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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: How to get Ada to "cross the chasm"? Date: Thu, 26 Apr 2018 21:38:00 +0200 Organization: Aioe.org NNTP Server Message-ID: References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <878t9nemrl.fsf@nightsong.com> <87h8o7lowg.fsf@nightsong.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> <87k1t1s9lx.fsf@nightsong.com> NNTP-Posting-Host: kQkuQcRDy1QFvWpyB1foYw.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 10.0; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 X-Notice: Filtered by postfilter v. 0.8.3 Content-Language: en-US Xref: reader02.eternal-september.org comp.lang.ada:51731 Date: 2018-04-26T21:38:00+02:00 List-Id: On 2018-04-26 19:38, Mehdi Saada wrote: > 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 ? It is impossible to prove everything, neither theoretically nor practically. Therefore the statement must be qualified - what is it you are going to prove. > 2) good idea, but badly integrated with the language ? It is an excellent idea. E.g. types conformance is proved because the language is statically typed and it is almost zero cost for the programmer. Other things may have low, medium, intolerably high cost or impossible. The language must allow to specify what exactly must be proved in the form of contract specification. > 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 ? In my view they have been focused on wrong things all the time since Ada 2005. E.g things like limited aggregates and return, dynamic predicates only diminish language soundness. > 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 ? There is no point in that critique unless they object all-or-nothing approach, which is then a tautology, because that thing is nonexistent anyway. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de