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!paganini.bofh.team!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Mon, 30 Apr 2018 14:40:39 -0500 Subject: Re: How to get Ada to "cross the chasm"? Newsgroups: comp.lang.ada 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> From: Norman Worth Date: Mon, 30 Apr 2018 13:40:39 -0600 User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:52.0) Gecko/20100101 Firefox/52.0 SeaMonkey/2.49.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <75mdnbuXAoiq7HrHnZ2dnUU7-fmdnZ2d@giganews.com> X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-Sn5lAY4mDI/PfXmsxtXhRSfANXI6FuPPQy1GxonbwEb9FUcd30iaDkEdjhZz/iY9b39qpEAVnYx3cqZ!LEo0JylY8Z2Qmd9pjInnboVhPFpgmmkZZwqaRsUAtM2AkXORIA6TwPuyOgQnexdR/GdY1jzNoEa6 X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 4150 Xref: reader02.eternal-september.org comp.lang.ada:51850 Date: 2018-04-30T13:40:39-06:00 List-Id: Randy Brukardt wrote: > "Mehdi Saada" <00120260a@gmail.com> wrote in message > news:d39f8a7e-1568-48a2-982d-f1ac6cecf975@googlegroups.com... >> 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 ? > > Pretty much all of the above. A lot of things aren't worth the effort to > prove (as Paul noted in his previous notes). At least not *special* effort. > Full algorithmic proof falls into this category for most things. OTOH, Ada > has a lot of information that the compiler uses to do essentially proofs to > make the code better. (Indeed, a tool like Codepeer is just an overgrown > compiler optimizer.) One can easily imagine feeding back that information to > the programmer to show problematic areas (that's what I'm trying to do with > future versions of Janus/Ada). > > Too much focus on static proving leads to neglecting what can be done with > dynamic checks and especially a combination of both. After all, Ada > compilers go to great lengths to eliminate dynamic checks; the checks that > can't be eliminated that way are potential problem areas. The same is true > for contracts. > > Anyway, I shouldn't talk too much about this as someone might actually do it > before I can get the time, and that would not be great. :-) > > Randy. > > > > Back when I was doing active programming, I ran into a problem, usually a small one, that required a formal proof about once a year. I did do programming that required reliable and proper results back then.