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: Thu, 26 Apr 2018 18:01:11 -0500 Organization: JSA Research & Innovation Message-ID: References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <87k1su7nag.fsf@nightsong.com> Injection-Date: Thu, 26 Apr 2018 23:01:12 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="3714"; 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:51735 Date: 2018-04-26T18:01:11-05:00 List-Id: "Paul Rubin" wrote in message news:87k1su7nag.fsf@nightsong.com... > "Randy Brukardt" writes: >>> C/C++ compilers for about USD 1.250. >> What's affordable? The Janus/Ada Personal Edition is still $195 > > Part of the thread context is that people want Ada 2012 and they want > SPARK. Janus Ada doesn't yet support Ada 2012 although I guess you > could use SPARK as an external verifier for Janus's Ada 95. It does support a small amount of Ada 2012 (aspects and libraries), and if I wasn't answering these sorts of messages, it probably would be supporting more. ;-) > Also, on the rrsoftware.com site I don't see Janus Ada offered for > anything but desktop computers. There's an unpursued opportunity in > embedded targets ;-). Seriously, that's how companies like Rowley > (rowley.co.uk) make a living. They don't try to compete with GCC on the > desktop. I don't know if Rational has any development budget these > days, but embedded is an area where Janus Ada could really do some good. We offer embedded kits, but those are much higher priced because of the greatly increased support requirements. (There is no such thing as an out-of-the-box embedded deployment, at least not commercially.) We used to have a number of customers on the 16-bit versions of that (mostly programming 186 chips), but those moved to other development systems when the 186 hardware was retired. Since then, I don't think anyone has even asked about it. (And of course any such system has to run on a desktop.) My goal from the very beginning was to bring structured, strongly typed programming to anyone needing to program. That hasn't changed, even though the programs have. These days, I'd expect Ada's biggest contribution (outside of embedded, an area that is well-covered by others) to be on (possibly distributed) server-side programs in client-server environments. The client should be very thin so Ada doesn't have much to offer there (unless you use Gnoga on the server and have no separate client at all). >> 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. > > Well, the discussion was about using SPARK to prove much more > complicated assertions. Again, why? > I agree that a decent type system is a big help > but a proof system goes a lot further. You can think of a proof system > as a type system that is Turing complete. That means you can verify > arbitrarily complex properties of a program, but (just like when you > proved theorems in math class) it's a lot of work, whose cost might or > might not be justified, depending. I'm not interested in a separate proof system, nor are most users interested. But a compiler does a lot of that stuff already (especially in the optimizer), and moreover, every Ada compiler does a lot of work to eliminate unneeded checks. It's not much of a leap to turn this into static checking in many cases (they'd have to be warnings in the Ada scheme of things, but that's not an real issue, since many compilers have warnings-are-errors as a standard mode). The beauty of this is that it allows people to ease into the checking of Ada, starting just with the type system and built-in checks, then adding subtypes with ranges, null exclusions, and eventually graduating to full use of Pre/Post and predicates. That's in part how I learned to love Ada; the longer I use it the more new ways I find to get Ada to do some of the checking for me. It's hard as heck to get people to change everything about their programming experience at once. Starting programmers out writing better-C-in-Ada-syntax and gradually letting them find about the other benefits that they can have is the way to hook them for life. (Although that often requires getting through to clueless management.) ... >> I assume you don't care much about software quality, because testing >> alone >> proves absolutely nothing. > > Oh come on, that's a platitude. Testing (if any tests pass) proves that > the program works at least some of the time. Careful testing proves (or > anyway gives good confidence) that the program works most of the time. > The actual meaning of your platitude is that testing can't prove that > the program never fails, so you have to think about your application's > failure tolerance. I don't really consider that testing. Moreover, modern programs almost completely defy the ability to be tested in any systematic way (see below). ... >> I don't even bother anymore on most of my code; if it runs, it works >> (or at least, it is assumed to work). > > Heh, are you telling me that Janus Ada has never been tested? Which one > of us did you say doesn't care about software quality? ;-) Janus/Ada is the exception -- I said "most". ;-) Even for Janus/Ada, I've long since given up on unit testing. Unit testing only works if it is run in a known environment (symbol table, source trees, etc.) Setting up that environment is a huge undertaking. Or you could just compile a targetted test program and all of that happens essentially for free. So testing Janus/Ada is using a large suite of tests (about 1400 tests plus the ACATS) to get reproduceable results. One can use tools to flag unusual results and essentially automate the process -- it takes about 4 hours to run these days (the early ACATS used to take 7 days to run on an early IBM PC -- machines have come a long way). But GUI programs are almost untestable in any repeatable way. I tried a number of tools to get repeatability, but they really didn't scale because the models would break every time something new got added. Maintaining the tests was more work than writing the program. (Most them are just maintaining configuration files anyway, so there is almost nothing else to test.) And as far as the servers go (web and mail), reproducible testing requires a stream of input. That's also a pain to create. So for most testing, I simply field them and let the Internet provide the stream of data. (I'm sane enough to keep the previous version around in case the new one turns out to be a brick, which happens more often than I care to admit.) I trust that the strong Ada error recovery and logging facilities will let me find any problems quickly, and usually without impacting most transactions. (Worst-case is a short-term denial of service.) That works in all of those cases because Ada detects a lot of problems at compile-time or runtime, so very little could happen that would actually be dangerous. (Obviously, if I was a bank, I might need to take a different approach.) Randy.