[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>
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



More information about the Rust-dev mailing list