clarify 'elements' of a type

[web.git] / ralf / _posts / 2017-07-17-types-as-contracts.md

diff --git a/ralf/_posts/2017-07-17-types-as-contracts.md b/ralf/_posts/2017-07-17-types-as-contracts.md
index 22a1fc2c153cc4025e240ec44c94bf7db492b344..125a1aa6b220aed6a94f1607f3a0c5b8c4635a6a 100644 (file)
--- a/ralf/_posts/2017-07-17-types-as-contracts.md
+++ b/ralf/_posts/2017-07-17-types-as-contracts.md
@@ -1,6 +1,7 @@
 ---
 title: "Types as Contracts"
 categories: internship rust
 ---
 title: "Types as Contracts"
 categories: internship rust

+forum: https://internals.rust-lang.org/t/types-as-contracts/5562

 ---
 
 Over the last couple of weeks of my [internship]({{ site.baseurl }}{% post_url
 ---
 
 Over the last couple of weeks of my [internship]({{ site.baseurl }}{% post_url


@@ -28,8 +29,8 @@ I'd like to propose that the fundamental reason this is UB is the *type* of the
 Borrowing some terminology from related fields, we can see the function type as stating a *contract*:  The `&mut` say that `simple` expects to be called with non-aliasing pointers.
 If we violate the contract, all bets are off.
 
 Borrowing some terminology from related fields, we can see the function type as stating a *contract*:  The `&mut` say that `simple` expects to be called with non-aliasing pointers.
 If we violate the contract, all bets are off.
 

-To realize this idea, we need to define, for every type, what is the contract associated with that type. When are elements of any given type *valid*?
-For some types, that's simple: `i32` is any four-byte value. `bool` is one byte, either `0` or `1`.
+To realize this idea, we need to define, for every type, what is the contract associated with that type. When is some piece of storage *valid* at any given type?
+For some types, that's simple: `i32` is any fully initialized four-byte value. `bool` is one byte, either `0` (representing `false`) or `1` (representing `true`).

 Compound types like `(T, U)` are defined in terms of their constituent types:  The first component must be a valid `T`, the second component a valid `U`.
 
 Where it gets interesting is the reference types: `&mut T` says that we have a (non-null, properly aligned) pointer.
 Compound types like `(T, U)` are defined in terms of their constituent types:  The first component must be a valid `T`, the second component a valid `U`.
 
 Where it gets interesting is the reference types: `&mut T` says that we have a (non-null, properly aligned) pointer.