Carter Schonwald <carter.schonw...@gmail.com>
wrote:
> enforce what statically? There is a very really very subtle tradeoff in
> how powerful a static verification scheme can be vs how easily it can be
> used (the sweet spot being somewhere in between nothing and complete
> proof based verification).
Enforce that integer overflow never happens.
Roughly, I was thinking of the following:
Every int variable/parameter/binding has an associated range (lower and
upper bound):
int<l,u>
If no bound is specified, the min and max values of the type are used.
Every operation on ints specify the range of the result using the range of
the operands:
int<l1,u1> + int<l2,u2> = int<l1+l2,u1+u2>
...
If the result does not fit into an int the compiler throws an error.
To resolve an error, you can:
- annotate the operands with appropriate bounds
- use a bigger type for the operation and check the result.
To go from a bigger to a smaller range you use:
let x : int
match x {
int<0,255> => ...
_ => fail()
}
Sorry for the sketchy syntax, I'm just following this list but have never
actually used rust.
> It sounds like there are valid arguments for several different error
> semantics for fixed size numbers, and those should perhaps be different
> builtin types. Everyone is right about the tradeoffs for their own needs,
> and choosing one semantics over another in that context is a mixed bag /
> iffy proposition. Tradeoffs are real, the best a language can do is make
> it easy to choose the right tradeoffs for you!
But also different languages choose different tradeoffs and rust aims to be
a systems PL.
By banning the fastest int version from the language by making overflow
wrapping or failing at runtime, you actually limit the choice already.
Tobi
_______________________________________________
Rust-dev mailing list
Rust-dev@mozilla.org
https://mail.mozilla.org/listinfo/rust-dev
