tag:blogger.com,1999:blog-9074318.post6984541732609163299..comments2011-08-23T05:39:20.128-04:00Michael Clopperthttp://www.blogger.com/profile/04478065709387726187noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-9074318.post-51293704448151687212008-12-08T20:11:00.000-05:002008-12-08T20:11:00.000-05:00Dean,<BR/><BR/>Absolutely agreed that there are practical limitations to contend with, but I think viewing unproven code as a fall-back position or lower-quality product is a good start. Just like anything in security, the ideal is unreachable, but this gives a very concise, understandable point we can aim at. Also remember that in this sense we are speaking of the science of computers. Theoretical computer science can be as far removed from practical development as applied physics can be from theoretical physics. But the theory shapes the understanding of the practitioners and future applications, and it is at that low of a level that I feel Dijkstra is correct in suggesting we re-evaluate the science.<BR/><BR/>For a sub-discipline that's made provable algorithms work, see: cryptography. Cryptographers can quickly point to just where their algorithms are and aren't provable. They know and understand the risks at a level rarely matched by other practitioners of computer science. No, all of our cryptographic systems aren't proven completely correct or sound, but going through the exercise of proof reveals where they may fail.Michael Clopperthttp://www.blogger.com/profile/04478065709387726187noreply@blogger.comtag:blogger.com,1999:blog-9074318.post-72233417271406215652008-12-08T10:21:00.000-05:002008-12-08T10:21:00.000-05:00It was an excellent read, and he's a genius, if only for search algorithms and leading the charge to stop using GOTO statements.<BR/><BR/>That said, we're talking about a man who didn't own or regularly use a computer until he needed one for email and web browsing. He didn't spend any time in the corporate world, and there's a significant cost/benefit analysis that you'd have to do before trying to implement his work. <BR/><BR/>For example, mathematically provable code is *not* easy to write. It's often easier in languages that aren't commonly used; Lisp and ML come to mind. It requires a level of rigor that many programmers simply aren't capable of, either.<BR/><BR/>Or, I think from the code-generation standpoint, provable code is useful for applications that *must* be perfect, but outside of that, it's a very questionable business move.<BR/><BR/>Although admittedly, there's a much stronger argument for it on the security side of the fence.Dean Jacksonhttp://www.blogger.com/profile/05862185746791036769noreply@blogger.com