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

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

"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87k1su7nag.fsf@nightsong.com...
> "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.

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.