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

Carter Schonwald carter.schonwald at gmail.com
Mon Jan 13 13:25:12 PST 2014


indeed, hence why i was saying there should be sized int variants for each
of those semantics (wrapping, trapping, overflowing, etc).
This is something that many people seem to favor, and is the right choice
for supporting smart engineers build reliable sophisticated software.
Namely, really spell out what each alternative means, make sure they're all
first class options, etc etc.

staticly verifying bounded ranges in a language is really subtle. You're
proposing what easily turns into a pretty tricky flow analysis (to have it
have any precision!), and it'd have to happen in type checker too...


On Mon, Jan 13, 2014 at 4:06 PM, Tobias Müller <troplin at bluewin.ch> wrote:

> 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
>
> _______________________________________________
> Rust-dev mailing list
> Rust-dev at mozilla.org
> https://mail.mozilla.org/listinfo/rust-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/rust-dev/attachments/20140113/92b08fdf/attachment.html>


More information about the Rust-dev mailing list