> What is important is that some magic formal tool could say that some > code in language "A", where bug of type "k" is possible, is not > equivalent to the version in language "B", where type "k" bugs are > impossible, ergo you have found a type "k" bug (in the absence of any > other bug in that section of code...).
Well, no. You know that a bug exists. It could be in one version (you don't know which one), or it could be in the verifier. If you assume that the verifier is bug-free, and you assume that the language-A version is semantically correct, then you know that a bug exists in the language-B version. It might be of type k or it might be of some other type (possibly a type that can exist in language A, possibly not). And in any case, you have not found it; you have only demonstrated its existence. /~\ 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
