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

["Randy Brukardt" <randy@rrsoftware.com>]

"Paul Rubin" <no.email@nospam.invalid> 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.
.