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