4 ms·

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

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

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.