Harvard vs. von Neumann

[dcrocker at eschertech.com (David Crocker)]

Crispin Cowen wrote:

> >
IMHO, all this hand wringing is for naught. To get systems that never fail
requires total correctness. Turing tells us that total correctness is not
decidable, so you simply never will get it completely, you will only get
approximations at best.
<<

What Turing actually tells us is that it is possible to construct programs that
may be correct but whose correctness is not decidable. This is a far cry from
saying that it is not possible to build well-structured programs whose
correctness _is_ decidable.

> >
Having humans write specifications and leaving programming to computers is
similarly a lost cause. At a sufficiently high level, that is asking the
computer to map NP to P, and that isn't going to happen.
<<

I don't understand what you are getting at here. If you are saying that humans
can map NP to P, but that it is impossible in principle to have computers do the
same thing, then that sounds like a religious argument to me. If you are saying
that you can write a specification that is unsatisfiable (or whose
satisfiability is undecidable) and that therefore cannot be implemented as code,
then this applies equally to human programmers. Incidentally, I have heard of a
few cases in which programming teams have wasted effort trying to implement sets
of requirements which, when the requirements were formalised, turned out to be
contradictory.

> >
At a less abstract level, you are just asking the human to code in a higher
level language. This will help, but will not eliminate the problem that you just
cannot have total correctness.
<<

The higher the level in which the human "codes", the less mistakes there are to
be made, assuming equal familiarity with the language etc. And you are just
repeating the same fallacious proposition by saying "you cannot have total
correctness". Had you instead said "you can never be sure that you have
established that the requirements capture the users' needs", I would have had to
agree with you.

> >
Programmable Turing machines are great, they do wonderful things, but total
correctness for software simply isn't feasible. People need to understand that
programs are vastly more complex than any other class of man made artifact ever,
, and there fore can never achieve the reliability of, say, steam engines.
<<

Same old flawed proposition. And, in software, the behaviour of the components
we build programs out of (i.e. machine instructions) are much more well-defined
and reliable than the materials that steam engines are built out of.

> >
The complexity of software is beginning to approach living organisms. People at
least understand that living things are not totally predictable or reliable, and
s**t will happen, and so you cannot count on a critter or a plant to do exactly
what you want. When computer complexity clearly exceeds organism complexity,
perhaps people will come to recognize software for what it is; beyond definitive
analyzability.
<<

Sure, if you develop a complex software system without a good design process
that carefully refines requirements to specifications to design to code - and
propagates changes in requirements down the chain too - then it may be
impossible to meaningfully analyse that software. That is why my approach is to
formalise requirements, write specifications that are proven to satisfy them,
then refine the specification to code - automatically where possible, but with
manual assistance where e.g. a data structure or an algorithm needs to be made
more efficient.

> >
We can never solve this problem. At best we can make it better.
<<

We can never solve the problem of being certain that we have got the
requirements right. I think that one implication for security is that there may
be whole new classes of threats out there that nobody has thought of yet, and
which we therefore can't refer to in the requirements. But we _can_ solve the
problem of ensuring that software meets the stated requirements, as long as
these are well-defined.

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com