X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/bac54ceb67ec86cfffadc8caaf4ff3c99c4a854d..b0eac911d950eb1982f5febf55fa2f20389ef8a7:/ralf/_posts/2018-08-22-two-kinds-of-invariants.md?ds=sidebyside

diff --git a/ralf/_posts/2018-08-22-two-kinds-of-invariants.md b/ralf/_posts/2018-08-22-two-kinds-of-invariants.md
index 2e4ff31..34f33bb 100644
--- a/ralf/_posts/2018-08-22-two-kinds-of-invariants.md
+++ b/ralf/_posts/2018-08-22-two-kinds-of-invariants.md
@@ -108,10 +108,11 @@ That is where safe code should be able to rely on safety, so that it can interac
 
 This is in strong contrast to validity, which must *always* hold.
 Layout optimizations and LLVM's attributes are in effect throughout unsafe code, so it is never okay to ever have invalid data.
+(With the sole restriction of data which *the compiler statically knows is not initialized*: If you write `let b: bool;`, that data in `b` is kept inaccessible *even to unsafe code*, and it does not have to satisfy any invariant. This works because the compiler knows about `b` not being initialized.)
 
 > *Unsafe code must always uphold validity invariants.*
 
-So we clearly cannot just pick the same invariant for both.
+So we clearly cannot just pick the same invariant for both, or else it would be impossible to write `Vec`.
 We *might* want to just ignore user-defined invariants when it comes to validity, but I think that would be ill-advised.
 
 First of all, validity is part of the definition of undefined behavior.
@@ -184,7 +185,7 @@ My gut feeling is that it should not be (i.e., validity should require that `i32
 I have talked about two kinds of invariants that come with every type, the safety invariant and the validity invariant.
 For unsafe code authors, the slogan summarizing this post is:
 
-> *You must always be valid, but you must only be safe in safe code.*
+> *You must always be valid, but you only must be safe in safe code.*
 
 I think we have enough experience writing unsafe code at this point that we can reasonably discuss which validity invariants make sense and which do not -- and I think that it is high time that we do so, because many unsafe code authors are wondering about these exact things all the time.