Re: How to get Ada to ?cross the chasm??

[Paul Rubin <no.email@nospam.invalid>]

"Randy Brukardt" <randy@rrsoftware.com> 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?  ;-)