diff --git a/slides/slides.tex b/slides/slides.tex
index 4240dcc..03896df 100644
--- a/slides/slides.tex
+++ b/slides/slides.tex
@@ -241,24 +241,6 @@ $1 = 84
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{Compilation Strategy}
 
-\begin{frame}{Interface: libunwind}
-    \begin{itemize}
-        \item \alert{libunwind}: \textit{de facto} standard library for
-            unwinding
-        \item Uses DWARF in background
-
-        \item \texttt{libunwind-eh\_elf}: alternative implementation using
-            \ehelfs{}
-
-        \item{} Result: \alert{alternative implementation} of libunwind, nearly
-            plug-and-play for existing projects!
-            \begin{itemize}
-                \item[$\leadsto$] It is \alert{easy} to use \ehelfs{}: just
-                    link against the right library!
-            \end{itemize}
-    \end{itemize}
-\end{frame}
-
 \begin{frame}{Compilation overview}
     \begin{itemize}
         \item Compiled to \alert{C code}
@@ -296,6 +278,24 @@ $1 = 84
     \end{itemize}
 \end{frame}
 
+\begin{frame}{Interface: libunwind}
+    \begin{itemize}
+        \item \alert{libunwind}: \textit{de facto} standard library for
+            unwinding
+        \item Uses DWARF in background
+
+        \item \texttt{libunwind-eh\_elf}: alternative implementation using
+            \ehelfs{}
+
+        \item{} Result: \alert{alternative implementation} of libunwind, nearly
+            plug-and-play for existing projects!
+            \begin{itemize}
+                \item[$\leadsto$] It is \alert{easy} to use \ehelfs{}: just
+                    link against the right library!
+            \end{itemize}
+    \end{itemize}
+\end{frame}
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{Outlining}
@@ -335,6 +335,19 @@ $1 = 84
     \lstinputlisting[language=C]{src/fib7/fib7.eh_elf_outline.c}
 \end{frame}
 
+\subsection{A word on formalization}
+
+\begin{frame}{A word on formalization}
+    \begin{itemize}
+        \item First task: \alert{writing semantics} for DWARF, written  as
+            mapping to C code.
+        \item DWARF5 specification: \alert{plain English}, no proper semantics
+        \item Compiled code is in substance equivalent to semantics
+        \item What remains to prove is mostly \alert{simple or classic
+            optimisations}
+    \end{itemize}
+\end{frame}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Benchmarking}
 
@@ -358,34 +371,20 @@ $1 = 84
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Unwinding using perf}
-
-\begin{frame}{Presentation of perf}
-    \textbf{A profiler is used to\ldots}
-    \begin{itemize}
-        \item get readings of the \alert{time spent in each function}
-        \item detect ``hot paths'': functions you ought to optimize
-        \item \ldots{}and \alert{benchmark \ehelfs{}}!
-    \end{itemize}
-
-    \vspace{1em}\pause{}
-    \textbf{How does it work?}
-    \begin{itemize}
-        \item{} \alert{Polling profiler}: stops at regular intervals to perform
-            analyses
-        \item{} Upon polling, \alert{dumps the stack} to a file
-        \item{} In the analysis phase (after the program terminated),
-            \alert{unwinds all the stacks gathered} to get call paths
-    \end{itemize}
-\end{frame}
-
 \begin{frame}{perf instrumentation}
+    \textbf{\alert{perf} is a polling profiler.}
+    \begin{itemize}
+        \item{} used to get readings of the time spent in each function
+        \item{} works by regularly stopping the program, unwinding its stack,
+            then aggregating the gathered data
+    \end{itemize}
+
+    \pause{}\bigskip{}
     \textbf{Instrumenting perf matches all the requirements!}
-    \vspace{1em}\pause{}
 
     \begin{itemize}
         \item{} \alert{Plug \ehelfs{} into perf}: use \ehelfs{} instead of
-            DWARF to analyze stack dumps
+            DWARF to unwind the stack
         \item{} Implement \alert{unwinding performance counters} inside perf
             \bigskip{}