[LLVMdev] Checked arithmetic

[John Regehr]

> Also, I think that a verified compiler is not the right goal. I think
> that what we want is a verifying compiler. We are not interested in
> whether the compiler is correct in any general sense. We are interested
> in whether the transformations performed by the compiler during some
> particular compilation are correct.

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:

http://pauillac.inria.fr/~xleroy/publi-by-topic.html#compcert

> That may be much easier to achieve, but I am not convinced that the LLVM
> team should adopt it as a goal. Their objectives are already complex
> enough.

I agree, I was thinking of this as a separate project based on a fork of 
LLVM.  If it happened to be wildly successful, some aspects could be 
folded back in.

John