Re: OO, C++, and something much better!

[dewar@merv.cs.nyu.edu (Robert Dewar)]

Bob Duff said

"It's incredible to me, and I don't count myself among the "test-debug
crowd".  I count myself among the "static type checking, and even
better, formal verification" crowd.  Nonetheless, whatever you've proven
at compile time, I want to see it work."

All I can say, is that people who have not tried this approach are usually
skeptical. Those who have tried it are less so, although in practice as
I mention earlier, usually the clean room approach does not eliminate
testing at a latter stage, it just eliminates testing as a development
tool.

I did try a no-testing approach on one Ada related project at Alsys (though
I did not tell people I was doing it!) I wrote the high precision arithmetic
support package for the Alsys Ada runtime, and quite deliberately decided
not to do any testing at all. I built semi-formal proofs of all the assembly
language involved (perhaps about 500 lines in total, so quite small), but
did not have access to any formal tools.

The resulting code was incorporated into a build that went to customers, and
the testing was minimal, since the ACVC suite did not excercise this 
functionality. I certainly did no testing. 

The bottom line was that this module was not error free, there was one
small error found about a year later, in a very obscure pathological
case that would not have been discovered by testing at least in my
opinion, even if that testing had been formalized to guarantee code
and path coverage (it was basically a problem of misunderstanding the
spec in an obscure case).

However, although not error free, this code was certainly as reliable or
more reliable than other code in the runtime, where we tool a more
traditional approach of relying on testing to a greater extent. It's hard
to say if it was more efficient, since I sure spent a lot of time on those
500 lines of code, but going through this excercise was certainly sufficient
to convince me that removing testing from the developers kit of tools is not
necessarily a terrible idea.

I definitely think that all students should be exposed to this approach.
I know that this is done at FIT (Florida Institute of Tech) in their
Software Engineering program. At first students are dismayed, even
distraught, at the idea of having to develop code without testing, but
by the end of the semester, they have amazed themselves by proving to
themselves that it is possible.

I am not arguing for a dogmatic "developers should be arrested if they
attempt to execute their code" approach, but it is a very good idea for
people to understand that formal reasoning and careful reading of code
*before* it is tested is a powerful tool for generating reliable software.
And this applies not matter *what* language things are written in, although
in practice some languages will encourage this approach more than others.
As I mentioned earlier, if you ask a roomful of Ada programmers how many
depend on the debugger, only about half will put up their hands, but if
you ask the same question of a roomful of Smalltalk or Lisp programmers,
you will get a *much* larger response, and indeed the question will strike
people as ludicrous.

Now I trust that there are indeed Smalltalk programmers who read their code,
and avoid over-dependence on testing and debugging, just as there are
certainly slash-and-burn-and-test-and-debug Ada programmers out ther, but
there is definitely an extent to which different languages encourage 
different styles of development.