4 ms·

I would say that SPJ was quite right, though. Compare and contrast with Haskell. In Haskell, there are broadly only three cases of unsoundness: * Infinite loop

I would say that SPJ was quite right, though. Compare and contrast with Haskell. In Haskell, there are broadly only three cases of unsoundness: * Infinite loops * `undefined` * Abuse of unsafe IO behavior, including monads built on or reducible to IO Rust's unsoundness bugs are all over [0], and come from so many different angles that they feel indistinct from any other low-level C-like language. I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt. [0] 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%... [1] https://gitlab.mpi-sws.org/iris/lambda-rust/tree/popl18 https://gitlab.mpi-sws.org/iris/lambda-rust/tree/popl18

rapsey 7y ago
You are being very disingenuous. Rust does not have unsound bugs all over stable. Linking to an issue tracker for bugs in development branch proves nothing.
- kibwen 7y ago
  As a Rust user, I think it's fine for the grandparent commenter to link to the I-unsound tag; even if some of those bugs are only accessible on the unstable nightly release, there are plenty of soundness bugs to choose from on the stable releases. The important thing is Rust's philosophy that soundness issues are to be taken seriously, even going so far as to allow backwards-incompatible changes if necessary to address them (though obviously this is a situation of last resort). There are several people working on formalizing aspects of Rust, and though it will take a long time to get there such efforts have already found and fixed bugs in Rust and its standard library. It's fair to take SPJ's critique on the chin for now; Rust deliberately chose the path of eventual soundness in order to produce a usable language in less time, and as long as we keep working towards that goal there's nothing to be ashamed about.
dranov 7y ago
> I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt. To clarify, we do have a work-in-progress formalization of pinning as part of RustBelt [0] (I worked on it over the summer). We did not discover this issue because RustBelt does not currently model traits, and the problem here is very much about the interaction between traits and pinning. Ralf touches on this in the linked discussion: > Actually trying to prove things about Pin could have helped, but one of our team actually did that over the summer and he did not find this issue. The problem is that our formalization does not actually model traits. So while we do have a formal version of the contract that Deref/DerefMut need to satisfy, we cannot even state things like "for any Pin<T> where T: Deref, this impl satisfies the contract". [0] - https://gitlab.mpi-sws.org/iris/lambda-rust/tree/gpirlea/pinning https://gitlab.mpi-sws.org/iris/lambda-rust/tree/gpirlea/pin...

rapsey 7y ago

You are being very disingenuous. Rust does not have unsound bugs all over stable. Linking to an issue tracker for bugs in development branch proves nothing.

kibwen 7y ago
As a Rust user, I think it's fine for the grandparent commenter to link to the I-unsound tag; even if some of those bugs are only accessible on the unstable nightly release, there are plenty of soundness bugs to choose from on the stable releases. The important thing is Rust's philosophy that soundness issues are to be taken seriously, even going so far as to allow backwards-incompatible changes if necessary to address them (though obviously this is a situation of last resort). There are several people working on formalizing aspects of Rust, and though it will take a long time to get there such efforts have already found and fixed bugs in Rust and its standard library. It's fair to take SPJ's critique on the chin for now; Rust deliberately chose the path of eventual soundness in order to produce a usable language in less time, and as long as we keep working towards that goal there's nothing to be ashamed about.

dranov 7y ago

> I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt. To clarify, we do have a work-in-progress formalization of pinning as part of RustBelt [0] (I worked on it over the summer). We did not discover this issue because RustBelt does not currently model traits, and the problem here is very much about the interaction between traits and pinning. Ralf touches on this in the linked discussion: > Actually trying to prove things about Pin could have helped, but one of our team actually did that over the summer and he did not find this issue. The problem is that our formalization does not actually model traits. So while we do have a formal version of the contract that Deref/DerefMut need to satisfy, we cannot even state things like "for any Pin<T> where T: Deref, this impl satisfies the contract". [0] - https://gitlab.mpi-sws.org/iris/lambda-rust/tree/gpirlea/pinning https://gitlab.mpi-sws.org/iris/lambda-rust/tree/gpirlea/pin...