3 ms·

> ...soundness is really a property of an entire interface. Not really. I mean, maybe... if you limit the scope of your consideration to language design itself

> ...soundness is really a property of an entire interface. Not really. I mean, maybe... if you limit the scope of your consideration to language design itself. If Rust call out to C code and they were using incompatible understanding of an array length due to mismatching build rules (like preprocessor definitions), you have a soundness bug it won't show up obviously in any interfaces anywhere. Soundness is a property of a single build of a program. You cannot generalize it. That is why in safety critical software, you cannot buy "safe" libraries or tools. You can buy libraries and tools with certification packets but context is very important when it comes to program correctness in all its forms.

oconnor663 4y ago
> Soundness is a property of a single build of a program. You cannot generalize it. I think it's important to be able to talk about sound functions, without needing to know anything about their callers, other than what's expressed in the function signature.
- humanrebar 4y ago
  I'm saying even for that case, you have to know how the implementation of that function was compiled, linked, and possibly even deployed. You cannot promise an interface is "sound". You can promise certain expectations were communicated clearly within some parameters (like object types and lifetimes assuming a coherent build process).
  - oconnor663 4y ago
    I think "soundness" is meaningful and useful in terms of the Abstract Machine that Rust is defined against. Or you know, the one that it will be defined against someday :) It's a way of separating things that are "under the language's control" in a sense from things that aren't. Just to pick an extreme example, if the `add` instruction is broken on my CPU, and it gives the wrong answer 0.001% of the time, and that causes my code to crash, is my code "unsound"? I think soundness/unsoundness just won't be a very useful idea if that's what we mean by it. Of course I do want my program to work, and I do need to fix things one way or another. I'm probably going to download a microcode update, or else throw my CPU in the trash, or possibly even turn on some special compiler workaround that avoids emitting `add`. But I think it's important and interesting to be able to talk about how I'm probably not going to fix my program by changing how I use the addition operator. There's really nothing wrong with my application code, even though my program isn't working. This is the sort of distinction that soundness is trying to draw.
    - humanrebar 4y ago
      There's something to that, but when an application and the libraries it uses don't agree on interfaces (ABIs, APIs, codecs, etc.) then the problem is unique to that project, and possibly that specific build of that project, so it's a little different than a buggy CPU. It's fair to try to simplify and tackle sets of distinct problems one at a time. Hence an abstract machine to assist in reasoning. But it's not the same as practical soundness or safety or whatever adjective people want to give. It's important to make that distinction because lightly technical people seem to ignore the subtlety here and think "well, it's a Rust program, therefore it's safe!". Reality is a lot more complicated. Unfortunately.
LegionMammal978 4y ago
> If Rust call out to C code and they were using incompatible understanding of an array length due to mismatching build rules (like preprocessor definitions), you have a soundness bug it won't show up obviously in any interfaces anywhere. In that scenario, I'd say that the build rules are a poorly-documented part of the C code's interface, and by calling out to it with mismatching build rules the Rust code is unsound. In general, C interfaces tend to have a lot of poorly-documented or undocumented preconditions, which is one of the things that make Rust-to-C FFI so tricky. One of Rust's big ideas is to make all these preconditions fully explicit, either through typestate or through "Safety" sections on unsafe functions and traits.
- humanrebar 4y ago
  Bad docs and brittle build expectations make C to C "ffi" tricky as well. But it's realistically how this kind of programming, generally speaking, tends to happen. I don't expect we'll have a great end to end solution until there are language agnostic build and dependency management systems available. As much as I like cargo, I don't expect porting everything to cargo will cut it. At least not in its current form.

oconnor663 4y ago

> Soundness is a property of a single build of a program. You cannot generalize it. I think it's important to be able to talk about sound functions, without needing to know anything about their callers, other than what's expressed in the function signature.

humanrebar 4y ago
I'm saying even for that case, you have to know how the implementation of that function was compiled, linked, and possibly even deployed. You cannot promise an interface is "sound". You can promise certain expectations were communicated clearly within some parameters (like object types and lifetimes assuming a coherent build process).
- oconnor663 4y ago
  I think "soundness" is meaningful and useful in terms of the Abstract Machine that Rust is defined against. Or you know, the one that it will be defined against someday :) It's a way of separating things that are "under the language's control" in a sense from things that aren't. Just to pick an extreme example, if the `add` instruction is broken on my CPU, and it gives the wrong answer 0.001% of the time, and that causes my code to crash, is my code "unsound"? I think soundness/unsoundness just won't be a very useful idea if that's what we mean by it. Of course I do want my program to work, and I do need to fix things one way or another. I'm probably going to download a microcode update, or else throw my CPU in the trash, or possibly even turn on some special compiler workaround that avoids emitting `add`. But I think it's important and interesting to be able to talk about how I'm probably not going to fix my program by changing how I use the addition operator. There's really nothing wrong with my application code, even though my program isn't working. This is the sort of distinction that soundness is trying to draw.
  - humanrebar 4y ago
    There's something to that, but when an application and the libraries it uses don't agree on interfaces (ABIs, APIs, codecs, etc.) then the problem is unique to that project, and possibly that specific build of that project, so it's a little different than a buggy CPU. It's fair to try to simplify and tackle sets of distinct problems one at a time. Hence an abstract machine to assist in reasoning. But it's not the same as practical soundness or safety or whatever adjective people want to give. It's important to make that distinction because lightly technical people seem to ignore the subtlety here and think "well, it's a Rust program, therefore it's safe!". Reality is a lot more complicated. Unfortunately.

LegionMammal978 4y ago

> If Rust call out to C code and they were using incompatible understanding of an array length due to mismatching build rules (like preprocessor definitions), you have a soundness bug it won't show up obviously in any interfaces anywhere. In that scenario, I'd say that the build rules are a poorly-documented part of the C code's interface, and by calling out to it with mismatching build rules the Rust code is unsound. In general, C interfaces tend to have a lot of poorly-documented or undocumented preconditions, which is one of the things that make Rust-to-C FFI so tricky. One of Rust's big ideas is to make all these preconditions fully explicit, either through typestate or through "Safety" sections on unsafe functions and traits.

humanrebar 4y ago
Bad docs and brittle build expectations make C to C "ffi" tricky as well. But it's realistically how this kind of programming, generally speaking, tends to happen. I don't expect we'll have a great end to end solution until there are language agnostic build and dependency management systems available. As much as I like cargo, I don't expect porting everything to cargo will cut it. At least not in its current form.