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!.POSTED!not-for-mail From: Paul Rubin Newsgroups: comp.lang.ada Subject: Re: How to get Ada to ?cross the chasm?? Date: Wed, 25 Apr 2018 18:45:59 -0700 Organization: A noiseless patient Spider Message-ID: <87k1su7nag.fsf@nightsong.com> References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: h2725194.stratoserver.net; posting-host="1130ff9118e09fa565bd1d3aa415c6bd"; logging-data="25086"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/KmO/GY0h6C8km7R+7Bbmr" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:bLSK7ja3XiP8ahpZCVbhMPAyDsg= sha1:GUUqmFHcYVyOMeVroBIfQ/8xAeY= Xref: reader02.eternal-september.org comp.lang.ada:51718 Date: 2018-04-25T18:45:59-07:00 List-Id: "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. 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. > 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. 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. > That might work for integers, but for real numbers such math has very > different characteristics and rules than the "usual" math. Definitely true, but a completely separate topic. > 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. If failure of the program can injure or kill someone, then as enlightenment philosophers and proof geeks we can say you need formal verification. Almost any other type of failure boils down to your losing some money (in many cases just the cost of releasing a fix). Deciding whether to deploy the software (and how much to spend on testing and/or verification) can then be seen as a betting proposition, where you evaluate likely costs, probabilities, etc., and make a rational choice. > 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? ;-)