[LLVMdev] Checked arithmetic

[Jonathan S. Shapiro]

On Thu, 2008-03-27 at 12:10 -0600, John Regehr wrote:
> > Don't forget prover. :-)
> 
> Say on that note here's something that I want to see: a formal semantics 
> for LLVM in for example higher order logic.  This would probably not be 
> that difficult.
> 
> The problem that this solves is that current verified compiler efforts 
> appear to be highly specific to both the language and the target.

Hmm. Maintaining this would impose a significant burden of long-term
stability on LLVM. From the rate of change that I see, I suspect that
Chris may not be ready to firm things up quite that much just yet.

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.

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.

shap