clarify

diff --git a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
index a95de96e45cb20c90507edb785b18b5e12750df9..5f0c07a98d1a45d033f938fb2ba6996b9ad641be 100644 (file)
--- a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
+++ b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
@@ -251,6 +251,7 @@ I am sure this will uncover bugs in corner-cases of my implementation, and it ma
 Speaking of the implementation, the problem around write locks described in [§2.1](21-suspension-of-write-locks) is not the only issue; another problem I still have to solve is to properly acquire and release locks on padding bytes and enum discriminants.
 
 While [§1.1](#11-ownership-passing-via-raw-pointers) is "fixed" by exempting unsafe code from the full range of checks, and the trouble with uninitialized memory ([§1.2](#12-uninitialized-memory)) will hopefully be solved as a side-effect of [changing the way uninitialized memory is handled](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung), this still leaves `Arc::drop` ([§1.3](13-arcdrop)) as an open problem.
 Speaking of the implementation, the problem around write locks described in [§2.1](21-suspension-of-write-locks) is not the only issue; another problem I still have to solve is to properly acquire and release locks on padding bytes and enum discriminants.
 
 While [§1.1](#11-ownership-passing-via-raw-pointers) is "fixed" by exempting unsafe code from the full range of checks, and the trouble with uninitialized memory ([§1.2](#12-uninitialized-memory)) will hopefully be solved as a side-effect of [changing the way uninitialized memory is handled](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung), this still leaves `Arc::drop` ([§1.3](13-arcdrop)) as an open problem.

+Notice that relaxing validation around unsafe code does not help here; the invalid data actually flows between functions, and so far the plan for unsafe code is to still enforce type validity when function boundaries are crossed.

 This comes down to a judgment call: We could relax validation sufficiently (e.g., relaxing validation in entire modules when they do certain unsafe things, and not validating private fields of structs that we cannot access) to make this code legal, or we could declare that code to actually be UB.
 The concrete problem in `Arc` can be fixed fairly easily as I have shown; the question is whether this kind of code is something that programmers actually expect to be legal -- and if they do, whether we can do anything about that (by providing documentation, or tools, or whatever else is necessary).
 Of course, it may also turn out that this shows that the entire approach is not actually feasible.
 This comes down to a judgment call: We could relax validation sufficiently (e.g., relaxing validation in entire modules when they do certain unsafe things, and not validating private fields of structs that we cannot access) to make this code legal, or we could declare that code to actually be UB.
 The concrete problem in `Arc` can be fixed fairly easily as I have shown; the question is whether this kind of code is something that programmers actually expect to be legal -- and if they do, whether we can do anything about that (by providing documentation, or tools, or whatever else is necessary).
 Of course, it may also turn out that this shows that the entire approach is not actually feasible.