Add notes

thesis/1-introduction.tex

@@ -297,12 +297,14 @@ These data structures are implemented using so-called \emph{raw pointers}. Raw p
 
 \subsection{(Other) Substructural Types}
 \begin{enumerate}
+    \item What are structural rules? Exchange, Weakening, Contraction
     \item Move semantics are affine types
     \item Clone and Copy is weakening
     \item \lstinline{#[must_use]} and relevant types
     \item Linear types
-    \item Ordered types
-    \item Uniqueness types
+    \item The borrow stack is ordered types
+    \item Uniqueness types:  There is only one reference (in contrast to linear types: no more references can be created)
+    \todo[inline]{Proof objects? Compile-time only linear values}
 \end{enumerate}
 
 \subsection{Purity and (algebraic) Effects}