ammendments go into the forum
[web.git] / ralf / _posts / 2017-07-17-types-as-contracts.md
index 22a1fc2..d11e77b 100644 (file)
@@ -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.
@@ -394,7 +395,7 @@ Congratulations!
 You have reached the end of this blog post.
 Thanks a lot for reading.
 If you have any comments, please raise them -- the entire purpose of this post is to get the proposal out there so that we can see if this approach can suit the needs of Rust programmers and compiler writers alike.
 You have reached the end of this blog post.
 Thanks a lot for reading.
 If you have any comments, please raise them -- the entire purpose of this post is to get the proposal out there so that we can see if this approach can suit the needs of Rust programmers and compiler writers alike.
-If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly.
+If there are explanations you think are missing or confusing, please bring that up as well; I may then update this post accordingly or add a note in the [forum](https://internals.rust-lang.org/t/types-as-contracts/5562) for any ammendments that turned out to be necessary.
 The concrete proposal will sure need some fixing here and there, but my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
 So, keep the comments flowing -- and safe hacking.
 
 The concrete proposal will sure need some fixing here and there, but my hope is that the general approach of a contract-like, type-driven validation mechanism ends up being useful.
 So, keep the comments flowing -- and safe hacking.