On Mon, 28 Nov 2005 08:44:04 +0000, Duncan Booth wrote: > Steven D'Aprano wrote: > >> Since real source code verifiers make no such sweeping claims to >> perfection (or at least if they do they are wrong to do so), there is >> no such proof that they are impossible. By using more and more >> elaborate checking algorithms, your verifier gets better at correctly >> verifying source code -- but there is no guarantee that it will be >> able to correctly verify every imaginable program. >> > I'm sure you can make a stronger statement than your last one. Doesn't > Godel's incompleteness theorem apply? I would have thought that no matter > how elaborate the checking it is guaranteed there exist programs which are > correct but your verifier cannot prove that they are.
Yes, of course. By saying "no guarantee" I was guilty of understatement: at the very least, we can guarantee that the verifier will *not* correctly verify every possible program. (Which of course is no different from human programmers.) -- Steven. -- http://mail.python.org/mailman/listinfo/python-list
