3 ms·

I think the argument is that if you said that about C++ everyone would be "yeah: this is just a useful tool, so why do I care?"... but Rust is about safety, and

by saurik 7y ago

I think the argument is that if you said that about C++ everyone would be "yeah: this is just a useful tool, so why do I care?"... but Rust is about safety, and if you don't have a formal model of the language by what reasoning could you possibly have to know it is safe? (And, in fact, every now and then--much less often these days, but still--someone finds a soundness issue in Rust itself, something you would hope to have been able to disprove at the outset using a proof over a formal model.)

mikekchar 7y ago
I know that "Rust is about safety" is the message that gets out, but I don't think it really is. At least, not any more than "Haskell is about safety". Rust is really about zero cost abstractions, IMHO. The borrow checker is a tool that allows you to work towards memory safety with zero cost abstractions. As a Rust developer, I'm actually much less worried about safety than I am about the zero cost. Rust allows me to achieve that zero cost without blowing up in complexity (which is sometimes hard to believe when you are wrestling with a borrow checker problem ;-) ). Having said that, I'm totally happy if there can be formal verification of these things. However, I certainly don't consider it to be job 1.
chrismorgan 7y ago
I care about Rust’s safety. It’s what let me confidently use Rust instead of Python or JavaScript, where I had never felt comfortable with C or C++. But the safety that Rust has already is good enough for me. I know that soundness holes exist (c.f. https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%92%A5 https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...), but they are very few, and if they’re realistic (most of those are possible but difficult to trigger and very unlikely to be encountered by real code) they get knocked down very quickly. Frankly I think you’re overhyping the benefits of a formal model (in practice I believe it’s normally only certain subsets of popular compilers that are ever formally verified), underestimating the pernicious presence of bugs even with formal verification, and overvaluing the significance of the remaining 0.00000001% of safety to a working programmer. In line with what mikekchar says, I care about performance and such things more than I care about formal verification of Rust’s safety. I’m happy to hear about this stuff, but I don’t expect it to personally affect me, for the better or for the worse.
_bxg1 7y ago
Not only that, it's much harder/impossible to implement an alternate compiler without a spec to go off of. C++ has multiple compilers which really benefits the ecosystem in various ways; until we have a spec, there's just rustc.

by saurik 7y ago

mikekchar 7y ago

I know that "Rust is about safety" is the message that gets out, but I don't think it really is. At least, not any more than "Haskell is about safety". Rust is really about zero cost abstractions, IMHO. The borrow checker is a tool that allows you to work towards memory safety with zero cost abstractions. As a Rust developer, I'm actually much less worried about safety than I am about the zero cost. Rust allows me to achieve that zero cost without blowing up in complexity (which is sometimes hard to believe when you are wrestling with a borrow checker problem ;-) ). Having said that, I'm totally happy if there can be formal verification of these things. However, I certainly don't consider it to be job 1.

chrismorgan 7y ago

I care about Rust’s safety. It’s what let me confidently use Rust instead of Python or JavaScript, where I had never felt comfortable with C or C++. But the safety that Rust has already is good enough for me. I know that soundness holes exist (c.f. https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%92%A5 https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...), but they are very few, and if they’re realistic (most of those are possible but difficult to trigger and very unlikely to be encountered by real code) they get knocked down very quickly. Frankly I think you’re overhyping the benefits of a formal model (in practice I believe it’s normally only certain subsets of popular compilers that are ever formally verified), underestimating the pernicious presence of bugs even with formal verification, and overvaluing the significance of the remaining 0.00000001% of safety to a working programmer. In line with what mikekchar says, I care about performance and such things more than I care about formal verification of Rust’s safety. I’m happy to hear about this stuff, but I don’t expect it to personally affect me, for the better or for the worse.

_bxg1 7y ago

Not only that, it's much harder/impossible to implement an alternate compiler without a spec to go off of. C++ has multiple compilers which really benefits the ecosystem in various ways; until we have a spec, there's just rustc.