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!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: How to get Ada to "cross the chasm"? Date: Thu, 26 Apr 2018 18:19:30 -0500 Organization: JSA Research & Innovation 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> Injection-Date: Thu, 26 Apr 2018 23:19:31 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="4188"; mail-complaints-to="news@jacob-sparre.dk" X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246 Xref: reader02.eternal-september.org comp.lang.ada:51736 Date: 2018-04-26T18:19:30-05:00 List-Id: "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.