Checked arithmetic

> Don't forget prover. :slight_smile:

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.

Once the semantics exists, you can either prove once and for all the that
each LLVM->LLVM optimization pass preserves the semantics of the code, or
else just do translation validation.

Verifying the LLVM->native backends should not be incredibly difficult.

Verifying a real LLVM front end would be a big projet but substantial
headway is being made on that kind of thing for example by Xavier Leroy's
group.

I've tried to sell some of the HOL folks on this idea (they have a formal
semantics for an ARM ISA, for example) but so far no dice.

John Regehr

Hi John,

some time ago I tried to encode some crucial properties
of LLVM IR in Omega (Tim Sheard's system). It looked
pretty good, but even encoding basic SSA properties as
types (i.e. may only reference an already defined variable)
cause your brain to overheat :slight_smile:

Stefan Monnier [1] has also some papers about provably correct
program transformations using an expressive type system.

Cheers,

  Gabor

[1] http://www.iro.umontreal.ca/~monnier/tcm.pdf