6 ms·

Simon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung an

Simon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung and others in the RustBelt project [1] did amazing work in formalizing Rust's safety guarantees, showing that Peyton Jones' guess was not accurate. There is nothing wrong about having bugs, of course, but the reaction to the bug in this thread shows that mathematical correctness is not as universally valued as I thought it would be. I agree with the sentiment that this is a bigger issue that shouldn't be discussed in a technical thread about a specific bug. However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases. Almost all of the popular languages don't care about this, for instance.) [0] https://youtu.be/t0mhvd3-60Y?t=130 https://youtu.be/t0mhvd3-60Y?t=130 [1] https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/

steveklabnik 7y ago
> However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases.) It's a balance. We cannot drop everything, nor stop all development, in order to get proofs. However, we are actively working toward formalizing the language itself, because we do see value in it.
- mauricioc 7y ago
  Totally reasonable stance, in my opinion, since Rust moves quickly and formalizing things takes time. But what is the stance on soundness bugs? Are they sometimes acceptable as permanent parts of the language, or is it a goal to eventually fix any soundness bugs that show up?
  - steveklabnik 7y ago
    Soundness bugs are the only thing we make an exception in our stability policy for. In general, unsoundness is treated as a serious issue. However, "unsoundness" can mean a few different things; in the "semantics of the language" sense, they're taken very seriously. In the "there's a compiler bug" sense, they're taken seriously, but in accordance with how likely they are to affect end users, and how much work they are to fix. For example, an incorrect type signature in the standard library was fixed one day after release by changing it to the correct one and re-releasing; an issue where casting between floating points and integers causes some problems has still not been fixed, because it partially has to do with LLVM's semantics combined with our semantics, and it's not clear how to do the right thing while not seriously regressing performance. (That being said that particular issue has had a flurry of activity in the past week...) The GitHub label for these bugs is A-Unsound, which has the description "A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness" https://en.wikipedia.org/wiki/Soundness".
    - mauricioc 7y ago
      Compiler bugs are not what I had in mind, so this answer is very reassuring! The original thread led me to believe this was not an absolute, official policy of the Rust project, but I am happy to hear it is.
      - steveklabnik 7y ago
        For more details, here's the written part of this: https://github.com/rust-lang/rfcs/blob/master/text/1122-language-semver.md#soundness-changes https://github.com/rust-lang/rfcs/blob/master/text/1122-lang... Please note that threads on internals are able to be posted to by anyone; things expressed there may not represent the way that the team feels about things.
  - Narishma 7y ago
    I believe soundness bug fixes are the only things allowed to break backwards compatibility in Rust.
  - 7y ago
- majewsky 7y ago
  If the formalization discovers more (or more significant) soundness holes, would that be a possible reason for a Rust 2.0 release?
  - steveklabnik 7y ago
    In theory, if there were incredibly massive holes that affected most Rust code and could not be fixed without backwards-incompatible changes, I guess so. Details matter in cases like these. It would just depend.
  - kibwen 7y ago
    This was something that kept me up at night in the run-up to Rust 1.0 and beyond (dreadful memories of the leakpocalypse), but so far we seem to have been quite lucky in that nobody has yet discovered a dramatic and fundamentally damning soundness flaw (and the progress of formal verification since 1.0 has increased confidence somewhat in the absence of such a flaw, but `Pin` represents a rather hairier increase in surface area than is usual... fingers crossed :P ).
- fluffything 7y ago
  > We cannot drop everything, nor stop all development, in order to get proofs. That kind of contradict some of the reactions, e.g., in this thread about adding an `Ordering::Unordered` to the language: https://internals.rust-lang.org/t/unordered-as-a-solution-to-bit-wise-reasoning-for-atomic-accesses/11079 https://internals.rust-lang.org/t/unordered-as-a-solution-to... Where it is essentially argued that "all development should be stopped until we have formal proofs". I guess it depends on which parts of the language things touch. `Ordering::Unordered` touches fundamentals parts of the memory model, and well, `Pin` touches the fundamental kinds of values that Rust has: owned, shared, mut shared, and with pin, also pinned. When people complain that things are stabilized too quickly, I don't think they complain about async / await taking years. The `Pin` API was unstable for like less than half a year in its final form before being stabilized, that's quite a short time for people to try to find holes in it, given how fundamental it is.
  - kibwen 7y ago
    Ralf is the one writing the soundness proofs (and bless him for doing so), but I don't believe that he's actually on the language team, so I wouldn't interpret that as an official stance.
  - steveklabnik 7y ago
    Team members can have their own opinion, of course. That is exactly what is happening in that thread, though Mazdak is the only language team member arguing that position. I personally wouldn't characterize this as "all development should be stopped until we have formal proofs," though, this argument is "if we commit to this API we will be locked out of one particular model and I'm not sure that we should be making that kind of decision yet." Empirically it's pretty clear that the language is being developed. If that were the decision of the team, it would pretty much have to go through an RFC, and so we'd be able to point to that.
lidHanteyk 7y ago
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...
dethinking 7y ago
Not sure if you caught it, but Ralf does address this somewhat in the thread: > Good question. We even had a sketch of a formal model for pinning, but that model was always about the three separate pointer types (PinBox<T>/PinMut<T>/Pin<T>). The switch to the generic Pin was done without formal modelling. > 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" That does sound scary, but I think the point is that this is a known blind spot in the formal model. It also has a known solution; the trait ought to be unsafe, so that the implementor takes responsibility for upholding the contract. The issue with Pin is it’s using an existing, safe trait, on the informal assumption that it couldn’t be unsoundly aliased by users. (Of course that turns out to be false.) So you can look at that and say “an unsound feature got into the stdlib without passing formal verification”, and that’s true, speaking to a lack of concern for formalization. On the other hand, you could look at it and say “the unsoundness of this feature is well isolated by formal methods and leakage at this interface is not the end of the world”, which is also true, and speaks to the utility of the formal work that has been done. It seems clear to me that the answer for Rust is “balance”. Formal verification is important not not to have, and things that can’t be verified shouldn’t be allowed. But formal verification takes up time when everything could be working 100% in production, and the alternative is likely even less sound formally, so it’s better to build an API now with some known risks than to wait for something known to be risk-free. Whatever your personal philosophy is, it seems clear that toeing that line has been instrumental to Rust’s success.
fluffything 7y ago
Two of Rust goals are: * Hack without fear (which can be interpreted as soundness) * Practical programming language (a language you can use to get stuff done) A full operational semantics of Rust with soundness proofs is probably at least a decade away, blocking the language on that would mean that one can't get anything done until that happens. And that is at tension with Rust being a practical language. So if you had a spectrum of languages, and you were to classify them along these two axes, Rust would be at the very safe and very practical end of the spectrum. But safety isn't an absolute, it's a spectrum. Rust won't protect you form, e.g., race conditions, dead locks, memory leaks, or somebody breaking into your house and hitting your computer with a baseball bat, etc. You need to have a threat model, and then deduce from it how much safety is enough. Rust aims to only give you memory and thread safety, so there is definitely room for much safer languages than Rust down the road, that protect you from these other things. The art is increasing safety, without sacrificing practicality, performance, etc.

steveklabnik 7y ago

> However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases.) It's a balance. We cannot drop everything, nor stop all development, in order to get proofs. However, we are actively working toward formalizing the language itself, because we do see value in it.

mauricioc 7y ago
Totally reasonable stance, in my opinion, since Rust moves quickly and formalizing things takes time. But what is the stance on soundness bugs? Are they sometimes acceptable as permanent parts of the language, or is it a goal to eventually fix any soundness bugs that show up?
- steveklabnik 7y ago
  Soundness bugs are the only thing we make an exception in our stability policy for. In general, unsoundness is treated as a serious issue. However, "unsoundness" can mean a few different things; in the "semantics of the language" sense, they're taken very seriously. In the "there's a compiler bug" sense, they're taken seriously, but in accordance with how likely they are to affect end users, and how much work they are to fix. For example, an incorrect type signature in the standard library was fixed one day after release by changing it to the correct one and re-releasing; an issue where casting between floating points and integers causes some problems has still not been fixed, because it partially has to do with LLVM's semantics combined with our semantics, and it's not clear how to do the right thing while not seriously regressing performance. (That being said that particular issue has had a flurry of activity in the past week...) The GitHub label for these bugs is A-Unsound, which has the description "A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness" https://en.wikipedia.org/wiki/Soundness".
  - mauricioc 7y ago
    Compiler bugs are not what I had in mind, so this answer is very reassuring! The original thread led me to believe this was not an absolute, official policy of the Rust project, but I am happy to hear it is.
    - steveklabnik 7y ago
      For more details, here's the written part of this: https://github.com/rust-lang/rfcs/blob/master/text/1122-language-semver.md#soundness-changes https://github.com/rust-lang/rfcs/blob/master/text/1122-lang... Please note that threads on internals are able to be posted to by anyone; things expressed there may not represent the way that the team feels about things.
- Narishma 7y ago
  I believe soundness bug fixes are the only things allowed to break backwards compatibility in Rust.
- 7y ago
majewsky 7y ago
If the formalization discovers more (or more significant) soundness holes, would that be a possible reason for a Rust 2.0 release?
- steveklabnik 7y ago
  In theory, if there were incredibly massive holes that affected most Rust code and could not be fixed without backwards-incompatible changes, I guess so. Details matter in cases like these. It would just depend.
- kibwen 7y ago
  This was something that kept me up at night in the run-up to Rust 1.0 and beyond (dreadful memories of the leakpocalypse), but so far we seem to have been quite lucky in that nobody has yet discovered a dramatic and fundamentally damning soundness flaw (and the progress of formal verification since 1.0 has increased confidence somewhat in the absence of such a flaw, but `Pin` represents a rather hairier increase in surface area than is usual... fingers crossed :P ).
fluffything 7y ago
> We cannot drop everything, nor stop all development, in order to get proofs. That kind of contradict some of the reactions, e.g., in this thread about adding an `Ordering::Unordered` to the language: https://internals.rust-lang.org/t/unordered-as-a-solution-to-bit-wise-reasoning-for-atomic-accesses/11079 https://internals.rust-lang.org/t/unordered-as-a-solution-to... Where it is essentially argued that "all development should be stopped until we have formal proofs". I guess it depends on which parts of the language things touch. `Ordering::Unordered` touches fundamentals parts of the memory model, and well, `Pin` touches the fundamental kinds of values that Rust has: owned, shared, mut shared, and with pin, also pinned. When people complain that things are stabilized too quickly, I don't think they complain about async / await taking years. The `Pin` API was unstable for like less than half a year in its final form before being stabilized, that's quite a short time for people to try to find holes in it, given how fundamental it is.
- kibwen 7y ago
  Ralf is the one writing the soundness proofs (and bless him for doing so), but I don't believe that he's actually on the language team, so I wouldn't interpret that as an official stance.
- steveklabnik 7y ago
  Team members can have their own opinion, of course. That is exactly what is happening in that thread, though Mazdak is the only language team member arguing that position. I personally wouldn't characterize this as "all development should be stopped until we have formal proofs," though, this argument is "if we commit to this API we will be locked out of one particular model and I'm not sure that we should be making that kind of decision yet." Empirically it's pretty clear that the language is being developed. If that were the decision of the team, it would pretty much have to go through an RFC, and so we'd be able to point to that.

lidHanteyk 7y ago

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

dethinking 7y ago

Not sure if you caught it, but Ralf does address this somewhat in the thread: > Good question. We even had a sketch of a formal model for pinning, but that model was always about the three separate pointer types (PinBox<T>/PinMut<T>/Pin<T>). The switch to the generic Pin was done without formal modelling. > 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" That does sound scary, but I think the point is that this is a known blind spot in the formal model. It also has a known solution; the trait ought to be unsafe, so that the implementor takes responsibility for upholding the contract. The issue with Pin is it’s using an existing, safe trait, on the informal assumption that it couldn’t be unsoundly aliased by users. (Of course that turns out to be false.) So you can look at that and say “an unsound feature got into the stdlib without passing formal verification”, and that’s true, speaking to a lack of concern for formalization. On the other hand, you could look at it and say “the unsoundness of this feature is well isolated by formal methods and leakage at this interface is not the end of the world”, which is also true, and speaks to the utility of the formal work that has been done. It seems clear to me that the answer for Rust is “balance”. Formal verification is important not not to have, and things that can’t be verified shouldn’t be allowed. But formal verification takes up time when everything could be working 100% in production, and the alternative is likely even less sound formally, so it’s better to build an API now with some known risks than to wait for something known to be risk-free. Whatever your personal philosophy is, it seems clear that toeing that line has been instrumental to Rust’s success.

fluffything 7y ago

Two of Rust goals are: * Hack without fear (which can be interpreted as soundness) * Practical programming language (a language you can use to get stuff done) A full operational semantics of Rust with soundness proofs is probably at least a decade away, blocking the language on that would mean that one can't get anything done until that happens. And that is at tension with Rust being a practical language. So if you had a spectrum of languages, and you were to classify them along these two axes, Rust would be at the very safe and very practical end of the spectrum. But safety isn't an absolute, it's a spectrum. Rust won't protect you form, e.g., race conditions, dead locks, memory leaks, or somebody breaking into your house and hitting your computer with a baseball bat, etc. You need to have a threat model, and then deduce from it how much safety is enough. Rust aims to only give you memory and thread safety, so there is definitely room for much safer languages than Rust down the road, that protect you from these other things. The art is increasing safety, without sacrificing practicality, performance, etc.