Re: Free C++compilers for a classroom
On 2007-09-27 12:09, Kai-Uwe Bux wrote:
robertwessel2@yahoo.com wrote:
On Sep 27, 3:51 am, James Kanze <james.ka...@gmail.com> wrote:
As I recall IBM tested the "no compiler" theory in Australia, and it
was a disaster... ;-)
As I recall, it's still being used for a number of critical
systems, where quality is of the utmost importance. It does
reduce the probability of an error in the final code somewhat,
but I'm not convinced that it's cost effective overall; a
compiler can check for things like typos a lot faster and a lot
cheaper than a code reviewer can.
The methodology is called "Cleanroom," and is moderately interesting,
since it's rather different than most of the other high-reliability
methodologies. And it focuses almost entirely on preventing bugs from
being introduced into the software project. Compiling and trying to
empirically determine if a piece of code works as expected is
considered wholly inadequate, rather the code must be proved correct
first. And frankly, if the code has compiler catchable syntax errors
in it, it's going to *way* fall short of that requirement.
Are you serious? You mean for each line they actually prove a lemma saying
that it has the required semicolon or curly brakets? Every time I have seen
or written a proof of correctness for a piece of code, the proof focused
entirely on semantics (because proofs are for humans and humans are
interested in understanding the semantics). I like proving things, and
there are parts of my code base that I only got correct when (after many
failures) I got down to proving them to work. However, such proves _never_
dealt with syntax errors.
I would suspect that the theory (and probably practice also) is that if
you have to write code the is provably correct you spend a lot of time
thinking about the code you are writing, so spending a little more to
make sure that the syntax is correct is no big loss. Also I would
suspect that you allow those syntax errors you write because the cost of
finding them through compilation is so low.
There is this story about Donald E. Knuth (I do not know if it is true
or not) where he participated in a programming contest, and he needed
the least amount of time to write the code, produced the best code, and
it all compiled and worked on the first try. His comment on the matter
was that when he learned to program you could not afford to write code
with bugs in it since compilation was to hand in the punch cards and
then wait a week to get the results back. If your code did not even
compile you had just wasted one week.
In any event, the requirement that the coder not be allowed to compile
or test their code (in some cases the dividing line is drawn on the
other side of the compile - IOW the testers cannot compile code, but
that doesn't make much difference) is not really the central point,
it's rather to prevent cheating by the programmers, who otherwise
could do some of their own compiles and unit testing and produce code
that will have a much lower defect density than equally unverified
code. That kills the tracking and feedback mechanism, which assumes
that the number of hard-to-find defects is related to the number of
easy-to-find defects in a predictable way, and by eliminating the
"easy" defects (IOW the ones the programmer will catch in the compile/
unit test cycle), you can no longer track the (hidden) hard-to-find
defects. If you could trust the programmers to accurately report all
those defects, the split would not be (as) necessary.
They've had some success (although like with all high reliability and
formally verified development methodologies, the cost is very high),
but I sure as heck would not like to work under those conditions.
By and large, I don't by this theory. When you try proving correctness of an
algorithm, it is very easy to fool yourself. Wrong proofs are as easy to
write as buggy programs. Moreover, it is _very_ hard to tell a wrong proof
from a correct one (because, contrary to popular belief, proofs are not
formal). It takes mathematicians several years of training to acquire that
skill (note: the most difficult part is to spot a bogus proof of a true
statement).
When dealing with any proof problem, you first toy around with examples and
convice yourself with moral arguments that some idea should work. Being
able to test those theories by implementating is invaluable for
understanding the problem. And that always comes first before you can hope
finding a solution (be that a proof or a program).
If this method yields better code quality, I would venture the conjecture
that it is not because the developers are denied access to compilers but
because they are given more time.
I know of only one place (though there must be several others) which
practice this methodology, and that is the guys who write the code used
in the US space shuttles. I would guess that most of them have at least
a PhD in formal software verification or similar, and as you said, they
have a lot of time.
--
Erik Wikstr??m