Re: Proving Correctness (was Java Portability)

["Warren W. Gay VE3WWG" <ve3wwg@home.com>]

nicolas wrote:
> "Warren W. Gay VE3WWG" <ve3wwg@home.com> a �crit dans le message news:
> 3B619A6D.5DD6E782@home.com...
> > I'd like to offer a slightly different "analogy" :
> >
> > _flamesuit on_
> >
> > The shopper looks at the Ada car, and notices that it has seatbelts and
> > of course 4 doors on it. The programmer says, but I don't want to be
> > restrained from accessing the outdoors -- I go through drive-throughs
> > a lot..
> >
> > The shopper than goes down the street and settles on the C++ car
> > which does not have the restrictive seat belts, and of course,
> > _NO_ doors to get in the way ;-)  The Java car has seatbelts, but
> > no doors...
> >
> > _flamesuit off_
> 
> I wouldn't see good and easy to use debuggers, standard libraries, GUI, IDE
> coming with the compiler, etc  ...
> as tools going against safety concerns ....

It's difficult for me to understand what the precise jist of your message
is here. One of the things you have meantioned here, suggest that you're
implying that YFL (your favourite language) provides a debugger, and so
that qualifies it to be just as safe as Ada. Am I reading too much into this?

This will be the only issue that I'll respond to here:

First of all, there are debuggers for Ada. The real issue however is more
along these lines, that an example might best highlight WRT safety :

Let's say your country has contracted two individuals to write a text based
chess program, that will compete in the global Chess Olympics (you are one
of the ones chosen and free to use YFL). The committee
is not sure what the implementation should be, but they want the 
final implementation to be rock solid, and
to not only obey all the rules of play under all circumstances, 
but it must not core dump.

Further, it must carry out an algorithm that 
has been designed by your country's sharpest chess master.

So you write a text based chess game in YFL (your favourite
language, but not Ada), according to the committees requirements.
You write the code, and eventually go through several iterations 
of testing in and out of YFD (your favourite debugger).

Now, another programmer uses Ada to accomplish the same task. He may well 
use a debugger, but he might not need it. This largely depends upon the 
skill of the programmer, of course, in any language. (This is just more
likely in Ada, but we can ignore this if it bothers you).

Now, both implementations are considered "complete" by their programmers,
and the sponsoring committee wants to have assurances from both, about
their correctness and readiness to carry out the chess match. The committee
must now choose which implementation to use. If the chosen implementation
should core dump, break a rule or fail performance wise, the country will
lose the match, with "egg on face." The chess master behind the software
chess algorithms will also lose face. Consequently, the committee is 
eager to choose the best implementation (it is "mission critical").

The non-Ada person has to submit that his program is correct on the basis
of testing. But the sponsoring committee asks "but how can you be sure
that you've done enough testing?" You might answer "there are too many
possibilities to check.. I cannot check all possibilities, but my testing
was _extensive_."

You're basically expecting to have the committee accept your implementation
on the basis that you tested "extensively" (the qualifications of the two
programmers where judged equal at the start).

The Ada person has the same challenge. He answers the sponsoring committee
that "I have tested _extensively_ and found no faults". But he can add
that "I have also had the source code audited by Ada professionals. This
has been done over and above what the 'computer' has checked at compile
time, during the project's development <insert Ada strengths about
strong type checking, module [package] isolation etc. etc.>."

The bottom line here is that Ada provides much greater assurances about
software correctness, than any other language that I am aware of. It is
also quite easy to read, making it easy to audit. Auditing C/C++ is a
nightmare, and easily error prone for humans. Java is an improvement, 
but still falls short.

In short, given that both implementations tested OK in front of the
committee, the committee chose to go with the Ada implementation. It's
not hard to see why.

The time is now past when people are concerned about efficiency. If it
is not already here, it will be here in a few more years as CPUs jump
another order of magnitude or so, forward in speed. 

As software becomes bloated by another order of magnitude (which ususally
follows CPU speed), then we'll be even more concerned about software 
reliability than ever before. We have built "towers of babel" on C/C++
frameworks. This is costly in security terms, and for reliability. If
we keep building "higher towers", we'll need more reliable footings
on which to build.

People abandoned assembly language for operating systems for the same
reasons. The time is coming when people will abondon C for operating
systems for "safer language".

Whether for applications or operating systems, I believe the time is
coming soon when people will be forced to look at Ada as an option
for building that next "big system".  People are already scratching
their heads in this area. At some point, the light bulb will start
going on and a few more people will discover Ada.  It is a language
that has already been designed to solve the problems that others are
looking for solutions in. It has the advantage that it has a lot
of experience, which is something that a designer of a new language
would be loath to throw away.

Some already have figured out, that Ada is a "good thing". More
will follow.

> Good luck if you want to convince Java or C++ programmers ... It could be a
> lot of fun, but I'm not sure they will even listen to you.

I was poking fun. I have to use C/C++ in my day job.

-- 
Warren W. Gay VE3WWG
http://members.home.net/ve3wwg