As far as I am aware, using theorem proving tools[1] to provide limits on value ranges is pretty hard and often computationally intensive to do in /simple/ code. I've only seen prototype systems where the user is expected to write full contracts on exactly how every function may modify every value it could, as well as often providing hints to the prover (especially for loops). So I really don't think this is going to help much.
[1]: https://en.wikipedia.org/wiki/Interactive_theorem_proving On Friday 20 Jun 2014 19:20:58 Gregory Maxwell wrote: > On Wed, Jun 18, 2014 at 10:08 AM, Gábor Lehel <glaebho...@gmail.com> wrote: > > core facts: wrapping is bad, but checking is slow. The current consensus > > On this point, has anyone tried changing the emitted code for all i32 > operations to add trivial checks, hopefully in a way that llvm can > optimize out when value analysis proves them redundant, which do > something trivial update a per task counter when hit and benchmarked > servo / language benchmark game programs to try to get a sane bound on > how bad the hit is even when the programmers aren't making any effort > to avoid the overhead? > _______________________________________________ > Rust-dev mailing list > Rust-dev@mozilla.org > https://mail.mozilla.org/listinfo/rust-dev
_______________________________________________ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
