4 ms·

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

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

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.