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!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.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: Wed, 25 Apr 2018 17:46:20 -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> Injection-Date: Wed, 25 Apr 2018 22:46:21 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="20560"; 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:51703 Date: 2018-04-25T17:46:20-05:00 List-Id: "Paul Rubin" wrote in message news:8736zqkwat.fsf@nightsong.com... >... > Those are intense requirements and it takes a lot of work to satisfy > them. If you aren't faced with those requirements, why do all that > work? Why do that work even if you have those those requirements? That's the beauty of Ada -- one can get static checking for essentially free from well-designed code. (And it's not appreciably harder than writing "typical" code.) You have to write assertions into your code in any case (if you want testing to actually be able to prove anything), so doing so in a structured manner seems like a win-win. > Non-realtime means you can use arbitrary precision arithmetic > (eliminating all those proofs about integer overflow) That might work for integers, but for real numbers such math has very different characteristics and rules than the "usual" math. It's trivially easy to use up vast amounts of memory that way. And the point is never to "eliminate proofs about overflow" but rather to get the right answer in a reasonable time. Almost every program written is soft-realtime in the sense that an answer is required immediately in a human time frame. (How long will you wait for a web page to load? Probably not more than a few seconds.) > and garbage > collection (automating memory management). If you are doing any memory management in Ada 2012, you had better have very strict requirements on time and/or space. Or be an Ada implementer. Otherwise, you are just an idiot. There are many good ways to write Ada 2012 code that don't involve any (explicit) memory management. (Local objects and containers being the best.) One almost never needs to use "new". > Realtime but non-critical > means you can get adequate reliability from traditional software testing > instead of proof systems. I assume you don't care much about software quality, because testing alone proves absolutely nothing. I don't even bother anymore on most of my code; if it runs, it works (or at least, it is assumed to work). That's in large part because my Ada compiler (and everybodies Ada compiler) detects many problems at compile-time and with good design will detect the majority of the rest at runtime. (The ones it can't detect are the cases when the wrong problem was solved, and no system could ever detect those.) The future of Ada (IMHO) is to move more of that runtime detection into the compiler, so that the benefits are essentially free and most importantly, can be gained incrementally. As you say, full verification will always be too expensive for most programs -- but that doesn't mean that you should then completely ignore the possibilities of proofs to detect bugs. For me, SPARK was always the wrong direction for Ada; it matters what gets done out of the box, not what some magical extra tool can do. Randy. .