Set up thesis document

thesis/1-introduction.tex

+\chapter{Introduction}
+
+\section{The Rust Ownership and Borrow System}
+
+\subsection{Ownership}
+\begin{enumerate}
+    \item Move semantics
+    \item Drop responsibilities
+    \item \lstinline{Clone} and \lstinline{Copy} (and \lstinline{Drop})
+\end{enumerate}
+\subsection{Borrowing}
+\begin{enumerate}
+    \item aliasing + mutability = race conditions
+    \item The borrow checker prevents this
+    \item two kinds of references
+    \item returning a borrow to the owner (lexical lifetimes)
+\end{enumerate}
+\subsection{Non-Lexical Lifetimes}
+\begin{enumerate}
+    \item Example: Correct but rejected program
+    \item Solution: Early drop of reference/non-lexical lifetimes
+\end{enumerate}
+\subsection{Reborrows and Two-Phase Borrowing}
+\begin{enumerate}
+    \item What is a reborrow?
+    \item Example: Reborrows are correct but rejected
+    \item Solution: Allow for Reborrows
+    \item Using shared references after creating a unique one is correct but rejected
+    \item Example
+    \item Solution: Two-Phase Borrowing
+    \item Note: This is not yet implemented
+\end{enumerate}
+\subsection{Loans and Regions}
+\begin{enumerate}
+    \item What are loans and regions?
+    \item regions as an alternative to lifetimes
+    \item regions are more powerful
+    \item Piggyback on the talk by \href{https://www.youtube.com/watch?v=_agDeiWek8w}{Niko Matsakis}
+    \item Note: Polonius will be a new Borrowchecker using regions but it is unstable
+    \item Note: concrete memory regions à la Cyclone vs abstract regions à la Polonius
+\end{enumerate}
+
+\section{Contracts and Refinement Types}
+\subsection{Contracts}
+\begin{enumerate}
+    \item Preconditions, Postconditions, Invariants
+    \item Hoare Logic
+    \item Contracts are a Runtime Check
+    \item Are there first-class contracts?
+    \item Higher-order contracts (\href{https://www2.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf}{Findler, Felleisen})
+\end{enumerate}
+\subsection{Refinement Types}
+\begin{enumerate}
+    \item Independent Refinement Types
+    \item Dependent Refinement Types/Refined Function Types
+    \item Refinement Types are “first-class”
+\end{enumerate}
+\subsection{Liquid Types SMT Solving}
+\begin{enumerate}
+    \item Refinement Types are not decidable
+    \item SAT is decidable
+    \item SMT is decidable
+    \item Liquid Types = $\{ RefinementType | decidable \}$
+\end{enumerate}
+\subsection{Hybrid Type Checking}
+\begin{enumerate}
+    \item Idea: Combine Contracts and Liquid Types
+    \item Sprinkle in casts everywhere an assertion is made
+    \item If the compiler can prove that this is ok or not ok, remove the cast (and potentially throw a compiler error)
+    \item All other casts are dynamic and lead to a panic if they fail.
+    \item In Rust, \lstinline{Result} and \lstinline{?} could be used instead. Problem: The error must be handled somewhere.
+\end{enumerate}
+
+\section{Other Extensions to a Type System}
+\subsection{Totality and Termination Metrics}
+\begin{enumerate}
+    \item Some functions can panic or loop indefinitely
+    \item In Rust, \lstinline{!} as return type helps (such a function does definitely not terminate)
+    \item There is no “may not terminate”, though, so you have to rely on the documentation
+    \item You can prove that a loop/recursion finishes by termination metrics
+    \item Panics can technically occur in every function (every function call needs memory space for a stack frame)
+    \item But you can prove that there are no “high-level” panics in any execution path within a function
+\end{enumerate}
+
+\subsection{Purity and (algebraic) Effects}
+\begin{enumerate}
+    \item Effects
+    \item Handling (Example: Exceptions)
+    \item Algebraic Effects
+    \item Pure functions don’t have unhandled effects
+    \item What counts as an effect (IO, allocation, computation)
+\end{enumerate}
+
+\subsection{(Other Substructural Types)}
+\begin{enumerate}
+    \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
+\end{enumerate}
\ No newline at end of file

thesis/thesis.tex

+% arara: lualatex
+% arara: biber
+% arara: lualatex
+% arara: lualatex
+
+\documentclass[a4paper, oneside, article]{memoir}
+
+\input{../preamble.tex}
+\includeonly{
+    1-introduction
+}
+
+\begin{document}
+
+\include{1-introduction}
+
+\end{document}
\ No newline at end of file