----- Original Message ----- > On Fri, Jul 13, 2012 at 1:40 AM, Andrew McCreight < > amccrei...@mozilla.com > wrote: > Type preserving compilers are pretty great, because you can spot a > large number of compiler bugs without even running the program > you've compiled, but due to the very new nature of Rust and the use > of LLVM as the backend it seems unsuitable for Rust. > > That's not necessarily so ... there has been interesting research, > which I can't find citations for right now, on retrofitting > certifying compilation to production compilers. Basically after each > code transformation pass you compare the before and after code and > use an inference procedure (possibly guided by breadcrumbs from the > transformation pass) to generate a proof that the code is equivalent > or at least preserves the properties you want.
Maybe you are thinking of translation validation [1]? (Amusingly, even CompCert is (or possibly was) a mixture of certified and certifying compilation, as it does not attempt to verify register allocation.) > I still think "make Servo actually work and be fast" >> "worry about > exploitable bugs in runtimes and JS JIT" >> "worry about bugs in the > Rust compiler". Definitely! It is interesting to ponder how the Servo risk profile will differ from the Firefox one. I think we'll find a larger percentage of security critical bugs for Servo in the Rust compiler than we do for Firefox in GCC/MSVC, both because the Rust compiler is younger, and because we're leaning on the safety guarantees provided by the runtime, but hopefully there will be less overall. Andrew [1] http://www.eecs.berkeley.edu/~necula/Papers/tv_pldi00.pdf _______________________________________________ dev-servo mailing list dev-servo@lists.mozilla.org https://lists.mozilla.org/listinfo/dev-servo
