bumper sticker slogan for secure software

[mouse at Rodents.Montreal.QC.CA (der Mouse)]

> 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               mouse at rodents.montreal.qc.ca
/ \ Email!           7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B