> IMO taking the compiler out of the trusted computing base is the way to go. That is the point of compiler verification after all. I'm biased here, but I thi

> IMO taking the compiler out of the trusted computing base is the way to go. That is the point of compiler verification after all. I'm biased here, but I think that another important point is to work out what the specification of a compiler is in the first place. Obviously, we've made a poor job of communicating this for C/C++, since so many people write broken code...