Harvard vs. von Neumann

[mouse at Rodents.Montreal.QC.CA (der Mouse)]

> 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.

True as far as it goes - but don't forget that you also haven't shown
the latter to be possible for programs of nontrivial size.

> The higher the level in which the human "codes", the [fewer] mistakes
> there are to be made, assuming equal familiarity with the language
> etc.

...but the more complex the "compiler", and the greater the likelihood
of bugs in it causing the resulting binary to fail to implement what
the human wrote.

> And you are just repeating the same fallacious proposition by saying
> "you cannot have total correctness".

It simply has not been formally established.  This does not make it
wrong, just unproven.  (Personally, I don't think it is wrong.)

> 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.

That too.

There are three places where problems can appear: (1) the
specifications can express something other than what the users
want/need; (2) the coders can make mistakes translating those
specifications to code; (3) the translation from code to binary can
introduce bugs.  (No, step (2) cannot be eliminated; at most you can
push around who "the coders" are.  Writing specifications in a formal,
compilable language is just another form of programming.)

I don't think any of these steps can ever be rendered flawless, except
possibly when they are vacuous (as, for exmaple, step 3 is when coders
write in machine code).

> > 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.

Same old *unproven* proposition.  Again, that doesn't make it wrong
(and, again, I don't think it *is* wrong).

> > 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.

We also can never solve the problem of being certain the conversion
from high-level language ("specifications", even) to executable code is
right, either.  Ultimately, everything comes down to "a lot of smart
people have looked at this and think it's right" - whether "this" is
code, a proof, prover software, whatever - and people make mistakes.

We're still finding bugs in C compilers.  Do you really think the
(vastly more complex) compilers for very-high-level specification
languages will be any better?

/~\ The ASCII                           der Mouse
\ / Ribbon Campaign
 X  Against HTML               mouse at rodents.montreal.qc.ca
/ \ Email!           7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B