Add chapter about how update type would look like in Rust (#17)

src/SUMMARY.md

@@ -26,6 +26,7 @@
 
 # Missing unsafe language constructs
 
+- [The update type](update-type.md)
 - [The robust keyword](robust-keyword.md)
 - [Proof fields](proof-fields.md)
 

src/quick-start.md

@@ -10,8 +10,7 @@ However, you may come back to it later for a quick refresher.
 The mental model relies on the following concepts. You don't need to understand ~~all of them~~ any
 of them. They are quite complicated. But knowing they exist is already a first step. You can just
 read through and skip anything you don't understand on first read:
-- There is a notion of **semantic types**. A semantic type is a set of execution states (this set
-  must satisfy some properties that we won't detail).
+- There is a notion of **semantic types**. A semantic type is a set of execution states.
 - Semantic types define a **contract** between parts of a program: the **producers** and the
   **consumers**. The contract is that, the producers must produce at most the execution states of
   the type, and the consumers must be able to consume at least the execution states of the type.

src/type-theory.md

@@ -22,6 +22,8 @@ The mental model is inspired by the following concepts:
   type interpretations: we are actually interpreting the whole typing, not just the type. This is
   only done for functional programming languages and would need to be adapted for imperative ones.
 - [RustHornBelt] for the idea of prophecies to explain the promised type of mutable references.
+- Refinement types which the update type is similar to. The main difference is that the update
+  refines the validity invariant, not the type itself.
 
 ## Breaking the dependency
 

src/update-type.md

@@ -0,0 +1,61 @@
+# The update type
+
+An attempt to add the update type to Rust could be something like this:
+
+```rust
+/// Generic wrapper over valid values of type T.
+///
+/// The predicate P describes which valid values are safe at the wrapped type.
+#[lang = "update"]
+#[repr(transparent)]
+pub struct Update<P, T> {
+    predicate: PhantomData<P>,
+    value: T,
+}
+
+impl<P, T> Update<P, T> {
+    /// Wraps a value.
+    ///
+    /// # Safety
+    ///
+    /// The predicate P must hold for the parameter.
+    ///
+    /// # Robustness
+    ///
+    /// - The parameter doesn't need to be a safe value.
+    /// - This is the identity function.
+    pub robust unsafe fn wrap(value: T) -> Self {
+        Update { predicate: PhantomData<P>, value }
+    }
+
+    /// Unwraps a value.
+    ///
+    /// # Robustness
+    ///
+    /// - The predicate P holds for the result.
+    /// - This is the identity function.
+    ///
+    /// # Safety
+    ///
+    /// The result is not necessarily a safe value.
+    pub robust unsafe fn unwrap(self) -> T {
+        self.value
+    }
+}
+```
+
+It's not clear what restrictions this type needs to have to be safe. It shouldn't implement any
+trait that provides safe access to the value (e.g. Deref and DerefMut). Producing (resp. consuming)
+an update type should always be unsafe because the predicate may be robust (resp. unsafe).
+
+## Examples
+
+Pin is a specific instance of the update type where `T` implements Deref and DerefMut in a specific
+way, such that implementing Deref and DerefMut for Pin is safe.
+
+```rust
+/// # Safety
+///
+/// If `T` implements Deref, it must not break "Pinned T". Idem for DerefMut.
+pub struct Pin<T>(Update<"Pinned T", T>);
+```