Skip to content

use sound/unsound terminology #164

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 4, 2019
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 12 additions & 8 deletions src/working-with-unsafe.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,14 @@ fn index(idx: usize, arr: &[u8]) -> Option<u8> {
}
```

This function is safe and correct. We check that the index is in bounds, and if it
is, index into the array in an unchecked manner. But even in such a trivial
function, the scope of the unsafe block is questionable. Consider changing the
`<` to a `<=`:
This function is safe and correct. We check that the index is in bounds, and if
it is, index into the array in an unchecked manner. We say that such a correct
unsafely implemented function is *sound*, meaning that safe code cannot cause
Undefined Behavior through it (which, remember, is the single fundamental
property of Safe Rust).

But even in such a trivial function, the scope of the unsafe block is
questionable. Consider changing the `<` to a `<=`:

```rust
fn index(idx: usize, arr: &[u8]) -> Option<u8> {
Expand All @@ -33,10 +37,10 @@ fn index(idx: usize, arr: &[u8]) -> Option<u8> {
}
```

This program is now unsound, and yet *we only modified safe code*. This is the
fundamental problem of safety: it's non-local. The soundness of our unsafe
operations necessarily depends on the state established by otherwise
"safe" operations.
This program is now *unsound*, Safe Rust can cause Undefined Behavior, and yet
*we only modified safe code*. This is the fundamental problem of safety: it's
non-local. The soundness of our unsafe operations necessarily depends on the
state established by otherwise "safe" operations.

Safety is modular in the sense that opting into unsafety doesn't require you
to consider arbitrary other kinds of badness. For instance, doing an unchecked
Expand Down