Remove the subsubsection on Dyon

In Dyon, a variable can be marked as outliving another one. I can’t see
how this is relevant, though. I don’t understand exactly how it works
but it seems to just increase a reference count/test that variables are
put on the stack in the right order, since there are no references. It
also seems to have non-local effects, which is double-plus-ungood.

thesis/1-introduction.tex

@@ -601,10 +601,6 @@ Since Polonius is still unstable and will be so for the forseeable future, there
 
 \emph{Cyclone} \cite{grossman2002region} is a dialect of C that introduces additional safe pointer types which are checked using regions. Instead of Polonius’ abstract regions, the regions in Cyclone represent concrete parts of memory.
 
-\subsubsection{Dyon}
-
-\todo[inline]{Maybe explain Dyon’s lifetimes as well? \inline{a : 'b} means “variable \inline{a} outlives variable \inline{b}”}
-
 \section{Contracts and Refinement Types}\label{sec:contracts-refinements}
 
 Every interface, be it a function, a library, or an \acs{HTTP} server, comes with a \emph{contract}: The interface expects data in a certain, well-defined form, and guarantees—given the input complies with this form—certain properties of the output. On the other hand, if the input is not well-formed, no guarantees on the output are made whatsoever. This principle is called “garbage in, garbage out”. If the interface exposes data, there are normally also some invariants that these data are supposed to conform to for the whole program run.