Restructure todos on 1.1.2

thesis/1-introduction.tex

@@ -209,7 +209,7 @@ Before we can discuss extensions to the borrow checker, let’s discuss naïve r
 let mut x = 0;
 {
     let xref = &x; // Create a reference to `x`
-    x += 1; // Error: Can’t mutate while a reference exists
+    x += 1; // Error: Cannot mutate while a reference exists
 }
 x += 1; // OK, no references exist anymore
 \end{lstlisting}
@@ -218,15 +218,19 @@ The program in \autoref{lst:lexical-lifetimes} is rejected by our naïve borrow
 
 \paragraph{Access Guards}\todo{Put this in an info box?}
 
-Sometimes we need access to a resource from multiple places at the same time, for example when sharing data between threads. For this, Rust provides the \lstinline{Mutex} container type. References to a mutex can be shared freely, but to change the value in the container, one has to acquire a lock, therefore making the access \emph{guarded}. While the mutex is locked, no other thread can access the data at all, a mutex lock is therefore similar to a \lstinline[language=Rust]{&mut} but its guarantees are enforced at runtime. The \lstinline{RwLock} type can give out both read and write locks which have behavior analogous to \lstinline[language=Rust]{&} and \lstinline[language=Rust]{&mut}, respectively. There are more constructs for similar use cases in the standard library, like \lstinline{Arc} and \lstinline{Cow}.
+Sometimes we need access to a resource from multiple places at the same time, for example when sharing data between threads. For this, Rust provides the \lstinline{Mutex} container type. References to a mutex can be shared freely, but to change the value in the container, one has to acquire a lock, therefore making the access \emph{guarded}.\todo{Add example} While the mutex is locked, no other thread can access the data at all, a mutex lock is therefore similar to a \lstinline[language=Rust]{&mut} but its guarantees are enforced at runtime. The \lstinline{RwLock} type can give out both read and write locks which have behavior analogous to \lstinline[language=Rust]{&} and \lstinline[language=Rust]{&mut}, respectively. There are more constructs for similar use cases in the standard library, like \lstinline{Arc} and \lstinline{Cow}.
+
+These data structures are implemented using so-called \emph{raw pointers}. Raw pointers, like pointers in C, are not borrow checked and can therefore alias. The programmer has to check manually that no rules are violated and should provide a safe interface that hides the raw pointers from the users. \todo{Pointers to Strict Provenance, Miri, …?}
+
+\paragraph{Returning references and Borrow-through}
+
+Functions can receive 
+
+\todo[inline]{Inferred lifetimes/Lifetime elision/Lifetime Polymorphism}
+
+\todo[inline]{Add paragraph on \lstinline{Borrow}, \lstinline{AsRef}, …?}
 
-These data structures are implemented using so-called \emph{raw pointers}. Raw pointers, like pointers in C, are not borrow checked and can therefore alias. The programmer has to check manually that no rules are violated and should provide a safe interface that hides the raw pointers from the users. \todo{Links to Strict Provenance, Miri, …}
 
-\begin{enumerate}
-    \item moving out of a borrowed value is illegal (e. g. \lstinline{let y = &x; let z = *y;})
-    \item lifetime polymorphism and lifetime elision
-          \todo[inline]{borrow-through}
-\end{enumerate}
 \subsection{Non-Lexical Lifetimes}
 \begin{enumerate}
     \item Example: Correct but rejected program
@@ -304,7 +308,7 @@ These data structures are implemented using so-called \emph{raw pointers}. Raw p
     \item Linear 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}
+          \todo[inline]{Proof objects? Compile-time only linear values}
 \end{enumerate}
 
 \subsection{Purity and (algebraic) Effects}