On: Rust is mostly safety

[lilyball]

What do you mean by "silent explicit type conversion"? If you said "silent type conversion" I'd read that as "implicit type conversion". But you said "explicit", which means you've got it very clearly in your code that you're doing a type conversion (to a smaller type), so what's silent about that?

[zzzcpan → lilyball]

Silent in terms of compiler not complaining.

[lilyball → zzzcpan]

Why would the compiler complain? Doing a narrowing type conversion is a perfectly legitimate thing to do. So when you ask the compiler to do it, it should.

[kbp → zzzcpan]

It forces you to explicitly say that you know you're forcing a value into a narrower type; I think the fact that might mean loss of information is understood, by definition. What would you like it to do?

[zzzcpan → kbp]

I would like it to tell me if I accidentally converted to a narrower type. This is a problem, because I don't necessary see the type I'm converting from due to type inference or simply am too far from the context where that type is declared and have to make assumptions to keep going. These assumptions of course fail sometimes and cause bugs. Same problem with precisions, by the way. I'm not sure how exactly compilers should fix this, the easiest fix seems to simply have different operators to explicitly allow lossy conversions, when necessary. But the bigger deal would be to treat numbers as sets of possible values with solvers or whatever to warn about mistakes where you use unhandled values in the code somewhere.

[iopq → zzzcpan]

Rust actually has this, this works:

    fn main() {
        let x = 5i32;
        let y: i64 = x.into();
        println!("{}", y);
    }

this doesn't work:

    fn main() {
        let x = 5i32;
        let y: i16 = x.into();
        println!("{}", y);
    }

you have to write:

    fn main() {
        let x = 5i32;
        let y = x as i16;
        println!("{}", y);
    }

where `as` has the potential of being lossy!

[icebraining → zzzcpan]

I agree that this is where we should be headed; it seems to me that Liquid Haskell, which was submitted to HN recently[1], could actually do what you need, since it uses an SMT solver to check for preconditions.

The casting function could specify the valid input values, and force the programmer to handle the rest of the cases when the input type is wider.

[1] https://news.ycombinator.com/item?id=13125328