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

Carter Schonwald carter.schonwald at gmail.com
Mon Jan 13 10:40:53 PST 2014


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).

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!

-Carter


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

> Daniel Micay <danielmicay at gmail.com> wrote:
> > On Sun, Jan 12, 2014 at 1:23 PM, Tobias Müller <troplin at bluewin.ch>
> wrote:
> >> Isaac Dupree
> >> <ml at isaac.cedarswampstudios.org> wrote:
> >>> In general, Rust is a systems language, so fixed-size integral types
> are
> >>> important to have.  They are better-behaved than in C and C++ in that
> >>> signed types are modulo, not undefined behaviour, on overflow.  It
> could
> >>> be nice to have integral types that are task-failure on overflow as an
> >>> option too.  As you note, bignum integers are important too; it's good
> >>> they're available.  I think bignum rationals would be a fine additional
> >>> choice to have (Haskell and GMP offer them, for example).
> >>
> >> Wrapping overflow is just as bad as undefined behavior IMO.
> >
> > Do you know what undefined behavior is? It doesn't mean unspecified.
>
> True, but despite beeing so often cited it won't format your hard disk
> (even in C).
> The result of an integer addition will always be an integer in every
> compiler I know so in this specific case I don't fear the UB.
>
> >> I cannot remember a single case of using signed integers where wrapping
> >> would make any sense.
> >
> > It often makes sense in codecs, hashing algorithms and cryptography.
>
> I'm sure there exist many cases where _unsigned_ int overflow makes sense.
> For _signed_ integers I'm a bit sceptical but I am no expert in that field.
>
> In any case it should not be the default but rather 'opt-in'.
>
> But this is not what I meant. Let me rephrase it differently:
> Assume that signed int overflow is UB (like in C). That means, all actual
> overflows at runtime have to be considered bugs.
> Now I cannot imagine any such case (bug) where guaranteed wrapping would
> actually behave nicer.
>
> > If you don't have clear bounds and don't want modular arithmetic, you
> > need big integers.
>
> Or proper input validation. The type defines the bounds.
>
> >> And you lose some optimization opportunities.
> >
> > It's treated as undefined because there are more optimization
> > opportunities that way.
>
> That's what I wanted to say. If you guarantee wrapping overflow you lose
> those opportunities.
>
> >> So why not take the path of the rust memory management and enforce
> bounds
> >> statically? It would need annotations on the types, like lifetimes, but
> it
> >> would be very rusty. Like C but safe.
> >
> > Rust isn't supposed to be really hard to write. Complex dependent typing
> would
>
> I'm not sure that this would be so complex. At least not more than the
> lifetime system. Is simple arithmetics on the bounds.
>
> In reality (rust beeing a systems PL) fixed width ints _will_ be used, and
> I am sure that overflow will often just be neglected. So why not enforce it
> statically?
>
> 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/effd5cb3/attachment-0001.html>


More information about the Rust-dev mailing list