\chapter{Formal Semantics for Combining OBS and Refinement Types}\label{ch:formal-semantics}
Our goal is to combine \acl{OBS} and refinement types introduced in \autoref{ch:introduction} into one semantics. In this chapter, we survey different kinds of formal semantics in general and semantics that already exist for Rust. We then discuss their amenability to extension with refinement types.
\section{Kinds of Formal Semantics}
\begin{enumerate}
\item Operational Semantics
\begin{enumerate}
\item big-step SOS
\item MSOS
\item small-step SOS
\item Reduction Semantics
\item Abstract Machine Semantics
\end{enumerate}
\item Denotational Semantics
\begin{enumerate}
\item Direct Style
\item Continuation-Passing Style
\item Continuation-Passing and RustBelt
\item Monadic Semantics
\end{enumerate}
\item Axiomatic Semantics and Hoare Logic
\item Action Semantics
\end{enumerate}
\section{Survey of Formal Semantics for Rust}
\begin{enumerate}
\item RustSem
\begin{enumerate}
\item language-independent Operational Semantics for OBS
\item Works on the \emph{Core Language} IR, which is closer to Rust than MIR
\item Implemented in the K framework
\end{enumerate}
\item Oxide
\begin{enumerate}
\item Not concerned with \inline{unsafe}, concurrency, sum types or traits
\item Region-based
\item Works on \emph{Oxide}, with an operational semantics on top of it
\end{enumerate}
\item Patina
\begin{enumerate}
\item Syntactic Borrow Checker
\item Works on a pre-1.0 version of Rust
\end{enumerate}
\item Featherweight Rust
\begin{enumerate}
\item\emph{FR} only does borrow checking, not typing
\item No NLL, closures, Branching, Products, or \inline{unsafe}
\item Small-step Operational Semantics
\end{enumerate}
\item KRust
\begin{enumerate}
\item Uses the K Framework
\item No traits/pattern matching
\item Term rewriting system
\end{enumerate}
\item RustHorn
\begin{enumerate}
\item Uses Constrained Horn Clauses
\item Problems with pointers
\end{enumerate}
\item Polonius
\begin{enumerate}
\item Operates on MIR/the CFG
\item Constraint solving using Datafrog
\end{enumerate}
\item Ferrocene
\begin{enumerate}
\item Limited formal specification
\item Only really a syntax for now, not a semantics
\end{enumerate}
\end{enumerate}
\section{Discussion}
\begin{enumerate}
\item Most semantics are too complicated
\item Polonius follows the control flow directly
\item Refinement type checking is also control flow sensitive
\item There is no formal semantics of Polonius, only a Datafrog model
\item Therefore, we need to transform Polonius into a “real” formal semantics