@@ -601,6 +601,10 @@ 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.
