[LLVMdev] Checked arithmetic

[Jonathan S. Shapiro]

On Thu, 2008-03-27 at 14:20 -0600, John Regehr wrote:
> My intuition is the same: translation validation sounds far easier than 
> compiler verification.  On the other hand general-purpose translation 
> validation does not exist (that I know of) whereas the compiler 
> verification people are making genuine steps forward.

Very interesting. Thanks for that pointer. It is surprising that one
problem is not a subset of the other.

One issue I did not mention: even if one decides only to emit a proof
for the transformation of the code that is emitted, one must still
verify the correctness of the IR reader (if applicable) and the code
emitter. A verified transformation of a low-confidence input would still
be a step forward, but the break in the confidence chain at the parser
is significant.

shap