News for hackers. Stuff that matters.

A comment on Unsoundness in Pin. Parent comment

Re:Unsoundness in Pin by lidHanteyk on Friday November 29, 2019 @10:23AM (#21664880)
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%...

[1] https://gitlab.mpi-sws.org/iris/lambda-rust/tree/popl18

[ Parent | on HN ]
Re:Unsoundness in Pin by dranov on Friday November 29, 2019 @11:27AM (#21665236)
> 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/pin...

[ Parent | on HN ]
Re:Unsoundness in Pin by rapsey on Friday November 29, 2019 @11:05AM (#21665118)
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.
[ Parent | on HN ]
Re:Unsoundness in Pin by kibwen on Friday November 29, 2019 @11:25AM (#21665226)
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.

[ Parent | on HN ]