> 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 [EMAIL PROTECTED]
/ \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B
_______________________________________________
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
_______________________________________________
