On Fri, Jul 13, 2012 at 1:40 AM, Andrew McCreight <[email protected]>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. 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". Rob -- “You have heard that it was said, ‘Love your neighbor and hate your enemy.’ But I tell you, love your enemies and pray for those who persecute you, that you may be children of your Father in heaven. ... If you love those who love you, what reward will you get? Are not even the tax collectors doing that? And if you greet only your own people, what are you doing more than others?" [Matthew 5:43-47] _______________________________________________ dev-servo mailing list [email protected] https://lists.mozilla.org/listinfo/dev-servo
