[rust-dev] Appeal for CORRECT, capable, future-proof math, pre-1.0

Tobias Müller troplin at bluewin.ch
Mon Jan 13 13:06:40 PST 2014

Carter Schonwald <carter.schonwald at gmail.com>
> 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):
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. 


More information about the Rust-dev mailing list