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.
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. 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. 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. 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. We can never solve this problem. At best we can make it better. Crispin -- Crispin Cowan, Ph.D. http://crispincowan.com/~crispin/ Director of Software Engineering http://novell.com AppArmor Chat: irc.oftc.net/#apparmor _______________________________________________ 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. _______________________________________________