From 54ce669c1b740df9f016046c671219f6fcb70fba Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 25 Aug 2019 12:52:16 +0200 Subject: [PATCH] use sound/unsound terminology --- src/working-with-unsafe.md | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/working-with-unsafe.md b/src/working-with-unsafe.md index 1864dd10..c29a75a5 100644 --- a/src/working-with-unsafe.md +++ b/src/working-with-unsafe.md @@ -16,10 +16,14 @@ fn index(idx: usize, arr: &[u8]) -> Option { } ``` -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 { @@ -33,10 +37,10 @@ fn index(idx: usize, arr: &[u8]) -> Option { } ``` -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