talk.tex

%% Style copied from https://github.com/omelkonian/presentations/tree/master/%5B2019.08.20%5D%20BitML%20(SRC%20Presentation%20%40%20ICFP))

\newif\iftalk
\newif\ifacm

\talktrue

%% \documentclass[aspectratio=43]{beamer}
\documentclass[aspectratio=169]{beamer}

\RequirePackage{ agda, tikz-cd, amssymb, catchfilebetweentags
               , newunicodechar , datetime2, geometry, relsize, xcolor
               , caption, subcaption, natbib }

\usetheme[
   block=fill,
   background=light,
   titleformat=smallcaps,
   progressbar=frametitle,
   numbering=none,
]{metropolis}%Warsaw,Madrid
\setbeamersize{text margin left=.5cm,text margin right=.5cm}

\usepackage[pdf]{graphviz}
\usepackage{tikz-cd}

%% \renewcommand\alert[1]{\textcolor{mLightBrown}{#1}}

\input{macros}

%% \usepackage{libertine}  %% [tt=false]

%% \setmathfont{XITSMath-Regular.otf}

%----------------------------------------------------------------------------

%% \titlegraphic{
%% \vspace*{7cm}
%% \includegraphics[keepaspectratio=true,height=1.4cm]{uu}
%% \hspace{1cm}
%% \includegraphics[keepaspectratio=true,height=1.4cm]{iohk}

\makeatletter
\def\zzpause{\ifmeasuring@\else\expandafter\pause\fi}
\makeatother

\begin{document}

\begin{center}
\setbeamerfont{title}{size=\large}
\setbeamerfont{subtitle}{size=\small}
\maketitle
\setbeamerfont{title}{size=\Large}
\setbeamerfont{subtitle}{size=\large}
\end{center}
\section{Preliminaries}
\begin{frame}{About Denotational Design}

  \begin{defn}
    \textbf{Denotational Design} is a type of thinking that prioirtizes thinking about the meaning and creating precise and elegant specifications using tools from abstract algebra and category theory.
\end{defn}
\pause
\begin{notn}
  In denotational design, the function $\llbracket \cdot \rrbracket$ is used to take any object to its meaning.
\end{notn}
\end{frame}

\begin{frame}{Motivations}
  \textbf{Why are we interested?} \pause
  Software and hardware engineering are built upon a tower of hodge-podge and ad-hoc foundations; desirable properties
  such as correctness are either not checked or not even specified
  \pause
  \begin{quote}
    ``That is not only not right; it is not even wrong''
    - Wolgang Pauli
\end{quote}
\pause
Using mathematics can return elegance to computation.
\end{frame}

\begin{frame}[fragile]{Philosophy}
\begin{columns}
\begin{column}{0.5\textwidth}

  % https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAB12BbOnACwBGA4ADkAviDGl0mXPkIoAzOSq1GLNpx78hoiVJnY8BImQBMq+s1aIO3XoOEAhMQD1CBkBiPyiyi9RWGrZaDrou7pLSXrLGCshmpAFq1mxRhnImKImUgeo2IJKqMFAA5vBEoABmAE4QXEiJIDgQSMopwSAA1AD6wKE6zm5gEtRwfFhVOEjEnrX1bdQtSACMeakh7AwMAjV0AMYA1jA4AASc+1AQZ5w1NbsHx9NzdQ2ITcuIZB0FnNsPRxO53Yl2uwLuAKe6RA8ze30+ax+bF6-Xsgz0oxADCwYAKcAg2Kg0NhSAALEtWogAKzUbG4thXHA4EogMYTKZIAC0K2+QV+Wx2e0BNxBjPB9yFULEFDEQA
  \begin{figure}
\begin{tikzcd}
\mathbb{N} \arrow[rrr, "+_{\mathbb{N}}"]                                               &  & {}                                                                  & \mathbb{N}                                             \\
                                                                                       &  &                                                                     &                                                        \\
\mathbb{B}^n \arrow[rrr, "+_{\mathbb{B}^n}"] \arrow[uu, "\llbracket \cdot \rrbracket"] &  & {} \arrow[uu, "\llbracket \cdot \rrbracket", dotted, shift left=6] & \mathbb{B}^n \arrow[uu, "\llbracket \cdot \rrbracket"]
\end{tikzcd}
\caption{A Diagram Showing the Relationship Between Representations and Meanings}
\figlabel{comm}
\end{figure}

\end{column}
\begin{column}{0.5\textwidth}  %%<--- here

We care about problems in \textbf{mathematics}, but our computations take place over \textbf{physics} (electrons, circuits).
\pause The denotation function $\llbracket \cdot \rrbracket$ gives us the meaning of any representation of electrons or bits.

\pause
\begin{qn}
What does it mean for a function over representations to be correct?
\end{qn}
\pause
\begin{thm}
  We say a function over representations is \textbf{correct} if \figref{comm} commutes, i.e. if
  \[\llbracket A +_{\mathbb{B}^{n}} B \rrbracket = \llbracket A \rrbracket +_{N} \llbracket B \rrbracket.\]
\end{thm}


\end{column}
\end{columns}
\end{frame}

\begin{frame}{Why Computer Arithmetic}
  Reasons why I chose computer arithmetic
  \begin{enumerate}
          \pause \item It is elementary; Most people have some exposure
          \pause \item It is a good way to show denotational design
    \end{enumerate}
    \pause The focus is not on any specific circuit component, but on specifications as to why it is \textbf{correct}
\end{frame}

\begin{frame}{Simplifications}
  For the purposes of this talk, I simplified from my paper:
  \begin{enumerate}
          \pause \item In my paper, I used the computer theorem prover language \textbf{Agda} to prove my propositions correct. You do not need to know programming for this talk.
          \pause \item In my paper, I talked about category theory, but for the sake of this talk, just imagine everything is occuring in the category of functions.
          \pause \item In my paper, I used little endian encoding, but in this talk, I will use big endian encoding because most people are probably more familiar with big endian.
        \end{enumerate}
\end{frame}


\begin{frame}{Binary Basics}

We will represent binary numbers as lists of bits, where the least significant bit is on the right (big endian encoding).

As an additional preliminary, we expect the reader to be familiar with common bitwise operations, including $\cdot \oplus \cdot$, $\cdot \lor \cdot$, and $\cdot \land \cdot$ (see table~\ref{table:bitops}).
\begin{notn}
  We use $N$ to denote our number system, we use $\mathbb{B}$ to represent a bit,  and we use $\mathbb{B}^{n}$ to denote an $n$-bit representation.
\end{notn}
\begin{table}[h]
\centering
\begin{tabular}{||c c c||}
 \hline
 $\cdot \oplus \cdot$ & $\cdot \lor \cdot$ & $\cdot \land \cdot$  \\ [0.5ex]
 \hline\hline
 $0 \oplus 0 = 0$ & $0 \lor 0 = 0$ & $0 \land 0 = 0$ \\
 $0 \oplus 1 = 1$ & $0 \lor 1 = 1$ & $0 \land 1 = 0$ \\
 $1 \oplus 0 = 1$ & $1 \lor 0 = 1$ & $1 \land 0 = 0$ \\
 $1 \oplus 1 = 0$ & $1 \lor 0 = 1$ & $1 \land 1 = 1$ \\
 \hline
\end{tabular}
\caption{$\cdot \oplus \cdot$, $\cdot \lor \cdot$, and $\cdot \land \cdot$}
\label{table:bitops}
\end{table}



\end{frame}

\section{Addition}

\begin{frame}{Converting $\mathbb{B}^{n}$ to $N$ }
  Anything we do is only correct modulo our meaning function $\llbracket \cdot \rrbracket$.
  \begin{align}
    \llbracket b_{n-1} \cdots b_{1} b_{0} \rrbracket
    &=  \llbracket b_{0} \rrbracket + 2 \llbracket b_{n-1} \cdots b_{1} \rrbracket \\
    \zzpause &= \llbracket b_{0} \rrbracket + 2 \llbracket b_{1} \rrbracket + 4 \llbracket b_{2} \rrbracket + \cdots + 2^{n-1} \llbracket b_{n-1 } \rrbracket
\end{align}
\pause
 \begin{figure}
   \digraph[width=.8\textwidth]{conversions}{
  node [shape=Mrecord]
  rankdir=LR
  input [label="{Input|{<in1>1|<in2>0|<in3>1}}"]
  add1 [label="{{<a11>1|<a12>4}|add|{<a1o>5}}"]
  dub1 [label="{{<dub11>2|<dub12>2}|add|{<dub1o>4}}"]
if1 [label="{{<if1i>1|1|0}|if|{<if1o>1}}"]
  output [label="{{<out>5}|output}"]
  if2 [label="{{<if2i>0|1|0}|if|{<if2o>0}}"]
  if3 [label="{{<if3i>1|1|0}|if|{<if3o>1}}"]
  add2 [label="{{<a21>0|<a22>2}|add|{<a2o>2}}"]
  add3 [label="{{<a31>1|<a32>0}|add|{<a3o>1}}"]
   dub2 [label="{{<dub21>1|<dub22>1}|add|{<dub2o>2}}"]
add1:a1o -> output:out [label="5"]
input:in1 -> if1:if1i  [label="1"]
if1:if1o -> add1:a11 [label="1"]
dub1:dub10 -> add1:a12 [label="3"]
input:in2 -> if2:if2i [label="0"]
input:in3 -> if3:if3i [label="1"]
if2:if2o -> add2:a21 [label="0"]
add2:a2o -> dub1:dub11 [label="2"]
add2:a2o -> dub1:dub12 [label="2"]
if3:if3o -> add3:a31 [label="1"]
add3:a3o -> dub2:dub22 [label="1"]
add3:a3o -> dub2:dub21 [label="1"]
dub2:dub2o -> add2:add22 [label="2"]
{rank=same; if1 if2 if3 }
   }
   \centering
   \caption{An Example showing $\llbracket 101 \rrbracket = 5$}
   \label{fig:conversionsbton}
\end{figure}

\end{frame}

\begin{frame}{Half-Adder Specification}

  A half adder is a function that adds two bits (possibly with a carry).
\begin{equation}
  \cdot +_{H} \cdot : \mathbb{B} \times \mathbb{B} \to \mathbb{B}^{2}
\end{equation}
  We need a correctness specification for a half-adder.
\pause
\begin{equation}\label{eqn:halfadder}
  \forall A,B \in \mathbb{B}^{1} \qquad \llbracket A +_{H} B \rrbracket = \llbracket A \rrbracket +_{N} \llbracket B \rrbracket
\end{equation}


\end{frame}

\begin{frame}{Half-Adder Example}
\begin{equation}\label{eqn:defhalfadd}
  \forall A,B\in \mathbb{B}^{1} \qquad A +_{H} B = (A \land B , A \oplus B)
\end{equation}
 \begin{figure}
   \digraph[width=.8\textwidth]{halfadder}{
  node [shape=Mrecord]
  rankdir=LR
  input [label="{Input|{<in1>1|<in2>1}}"]
  output [label="{{<out2>1|<out1>0}|output}"]
    xor [label="{{<xi1>1|<xi2>1} | xor | {<xo>0}}"]
    and [label="{{<ai1>1|<ai2>1} | and | {<ao>1}}"]
    input:in1 -> xor:xi1 [label="1"]
    input:in2 -> xor:xi2 [label="1"]
    input:in1 -> and:ai1 [label="1"]
    input:in2 -> and:ai2 [label="1"]
     xor:xo -> output:out1 [label="0"]
    and:ao -> output:out2 [label="1"]
   }
   \centering
   \caption{An Example Showing $1 +_{H} 1 = 10$}
   \label{fig:halfadder}
\end{figure}



\end{frame}

\begin{frame}{Full-Adder Specification}
  A full-adder adds $3$ bits with possibly a carry.
  \begin{equation}
    +_{F}(\cdot , \cdot , \cdot) : \mathbb{B} \times \mathbb{B} \times \mathbb{B} \to \mathbb{B}^{2}
\end{equation}
\begin{equation}\label{eqn:fulladderspec}
  \forall A,B, C \in \mathbb{B}^{1} \qquad \llbracket +_{F}(A,B,C) \rrbracket  = \llbracket A \rrbracket  + \llbracket B \rrbracket + \llbracket C \rrbracket
\end{equation}

\end{frame}

\begin{frame}{Full-Adder Example}
\begin{equation}\label{eqn:fulladderdef}
  \forall A,B,C \in \mathbb{B}^{1} \qquad +_{F}(A,B,C) = (A \land B \lor (A \oplus B) \land C , A \oplus B \oplus C )
\end{equation}
 \begin{figure}
   \digraph[width=\textwidth]{fulladder}{
  node [shape=Mrecord]
  rankdir=LR
  input [label="{Input|{<in1>1|<in2>0|<in3>1}}"]
  output [label="{{<outc>1|<outs>0}|output}"]
    ad1 [label="{{<a11>1|<a12>0} | half-adder | {<a1c>0|<a1s>1}}"]
    ad2 [label="{{<a21>1|<a22>1} | half-adder | {<a2c>1|<a2s>0}}"]
    or [label="{{<oi1>0|<oi2>1} | or | {<oo>1}}"]
    input:in1 -> ad1:a11 [label="1"]
    input:in2 -> ad1:a12 [label="0"]
   input:in3 -> ad2:a22 [label="1"]
ad1:a1s -> ad2:a21 [label="1"]
ad2:a2s -> output:outs [label="0"]
ad2:a2c -> or:oi2 [label="1"]
ad1:a1c -> or:oi1 [label="0"]
or:oo -> output:outc [label="1"]
   }
   \centering
   \caption{An Example Showing $+_{F}(1,0,1) = 10$}
   \label{fig:fulladder}
\end{figure}

\end{frame}

\begin{frame}{Ripple Adder Specification}
  \begin{equation}
    \cdot +_{\mathbb{B}^{n}}^{\cdot} \cdot : \mathbb{B}^{1} \times \mathbb{B}^{n} \times \mathbb{B}^{n} \to \mathbb{B}^{n+1}
    \end{equation}

    \begin{equation}
      \forall A , B \in \mathbb{B}^{n} \quad \forall C \in \mathbb{B}^{1} \qquad \llbracket A +_{\mathbb{B}^{n}}^{C} B \rrbracket = \llbracket A \rrbracket +_{N} \llbracket B \rrbracket +_{N} \llbracket C \rrbracket
    \end{equation}
\end{frame}

\begin{frame}{Ripple Adder Specification}

\begin{table}
 \begin{tabular}{c|c|c|c}
     ${}^1$ & ${}^11$    &${}^1 0$    &1\\
     + & 1      & 1    & 1 \\ \hline
    1 & 1    & 0    &0\\ \hline
 \end{tabular}
 \centering
 \caption{Grade-School Addition}
 \label{tab:gradeschooladdition}
\end{table}
\begin{equation}\label{eqn:RCA}
  \begin{split}
  a_{n-1}\cdots a_{2}a_{1}a_{0} +_{\mathbb{B}^{n}}^{c_{0}} b_{n-1} \cdots b_{2}b_{1}b_{0} = (a_{n-1} \cdots a_{2}a_{1} +_{\mathbb{B}^{n-1}}^{c_{1}} b_{n-1} \cdots b_{2}b_{1})  r_{0} \\
  \text{where}\\
   c_{1}r_{0} = +_{F}(a_{0}, b_{0}, c_{0})
    \end{split}
  \end{equation}
\end{frame}
\begin{frame}{Ripple Adder Picture}
 \begin{figure}
   \digraph[width=\textwidth]{bitadder}{
node [shape=Mrecord]
  rankdir=LR
  input1 [label="{Input 1|{<i11>1|<i12>0|<i13>1}}"]
input2 [label="{Input 2|{<i21>1|<i22>1|<i23>1}}"]
  output [label="{{<o1>1|<o2>1|<o3>0|<o4>0}|Output}"]
  f1 [label="{{<f11>1|<f12>1|<f13>0}|Full-Adder|{<f1c>1|<f1s>0}}"]
  input1:i13 -> f1:f11 [label="1"]
  input2:i23 -> f1:f12 [label="1"]
  f1:f1s -> output:o4 [label="0"]
  f2 [label="{{<f21>0|<f22>1|<f23>1}|Full-Adder|{<f2c>1|<f2s>0}}"]
input1:i12 -> f2:f21 [label="0"]
  input2:i22 -> f2:f22 [label="1"]
  f1:f1c -> f2:f23 [label="1"]
  f2:f2s -> output:o3 [label="0"]
    f3 [label="{{<f31>1|<f32>1|<f33>1}|Full-Adder|{<f3c>1|<f3s>1}}"]
input1:i11 -> f3:f31 [label="1"]
  input2:i21 -> f3:f32 [label="1"]
  f2:f2c -> f3:f33 [label="1"]
  f3:f3s -> output:o2 [label="1"]
  f3:f3c -> output:o1 [label="1"]
   }
   \centering
   \caption{An Example Showin $101 +_{\mathbb{B}^{3}}^{0} 111 = 1100 $}
   \label{fig:RCA}
\end{figure}


\end{frame}

\begin{frame}{Ripple Adder Proof}

\begin{proof}
  Induct on $n$. If $n=1$, we just have a full-adder. Otherwise, let $n = n + 1$.
  \begin{align}
    &\llbracket a_{n}\cdots a_{2}a_{1}a_{0} +_{\mathbb{B}^{n+1}}^{c_{0}} b_{n} \cdots b_{2}b_{1}b_{0} \rrbracket\\
   \zzpause &= \llbracket (a_{n} \cdots a_{2}a_{1} +_{\mathbb{B}^{n}}^{c_{1}} b_{n} \cdots b_{2}b_{1})  r_{0}  \rrbracket \\
    \zzpause &= 2\llbracket a_{n} \cdots a_{2}a_{1} +_{\mathbb{B}^{n}}^{c_{1}} b_{n} \cdots b_{2}b_{1} \rrbracket + \llbracket  r_{0}  \rrbracket \\
     \zzpause &= 2 (\llbracket a_{n} \cdots a_{2}a_{1} \rrbracket  +  \llbracket b_{n-1} \cdots b_{2}b_{1} \rrbracket + \llbracket c_{1} \rrbracket ) + \llbracket  r_{0}  \rrbracket \\
      \zzpause&= 2 \llbracket a_{n} \cdots a_{2}a_{1} \rrbracket  +  2\llbracket b_{n-1} \cdots b_{2}b_{1} \rrbracket + 2\llbracket c_{1} \rrbracket + \llbracket r_{0} \rrbracket \\
      \zzpause&= 2 \llbracket a_{n} \cdots a_{2}a_{1} \rrbracket  +  2\llbracket b_{n-1} \cdots b_{2}b_{1} \rrbracket + \llbracket c_{1}r_{0} \rrbracket \\
    \zzpause  &= 2 \llbracket a_{n} \cdots a_{2}a_{1} \rrbracket  +  2\llbracket b_{n-1} \cdots b_{2}b_{1} \rrbracket + \llbracket +_{F}(a_{0}, b_{0}, c_{0}) \rrbracket \\
    \zzpause  &= 2 \llbracket a_{n} \cdots a_{2}a_{1} \rrbracket  +  2\llbracket b_{n-1} \cdots b_{2}b_{1} \rrbracket + \llbracket a_{0} \rrbracket + \llbracket b_{0}\rrbracket + \llbracket c_{0} \rrbracket \\
    \zzpause  &= 2 \llbracket a_{n} \cdots a_{2}a_{1} \rrbracket + \llbracket a_{0} \rrbracket +  2\llbracket b_{n-1} \cdots b_{2}b_{1} \rrbracket + \llbracket b_{0} \rrbracket  + \llbracket c_{0} \rrbracket \\
     \zzpause &= \llbracket a_{n} \cdots a_{2}a_{1}a_{0} \rrbracket + \llbracket b_{n} \cdots b_{2}b_{1}b_{0} \rrbracket + \llbracket c_{0} \rrbracket
\end{align}
\end{proof}
\end{frame}

\section{Multiplication}

\begin{frame}[fragile]{Multiplication Specification}
  Before we implement multiplication, we first need a specification.
  \pause The specification for multiplication is very similar to that of addition.
  \pause
  \[\forall A \in \mathbb{B}^{m} \quad B \in \mathbb{B}^{n} \qquad \llbracket A \times_{\mathbb{B}^{m,n}} B \rrbracket = \llbracket A \rrbracket \times_{N} \llbracket B \rrbracket\]

  % https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAB12BbOnACwBGA4ADkAviDGl0mXPkIoAzOSq1GLNpx78hoiVJnY8BImQBMq+s1aIO3XoOEAhMQD1CBkBiPyiyi9RWGrZaDrou7pLSXrLGCshmpAFq1mxRhnImKImUgeo2IJKqMFAA5vBEoABmAE4QXEiJIDgQSMopwSAA1AD6wKE6zm5gEtRwfFhVOEjEnrX1bdQtSACMeakh7AwMAjV0AMYA1jA4AASc+1AQZ5w1NbsHx9NzdQ2ITcuIZB0FnNsPRxO53Yl2uwLuAKe6RA8ze30+ax+bF6-Xsgz0oxADCwYAKcAg2Kg0NhSAALEtWogAKzUbG4thXHA4EogMYTKZIAC0K2+QV+Wx2e0BNxBjPB9yFULEFDEQA
  \begin{figure}
\begin{tikzcd}
\mathbb{N} \arrow[rrr, "\times_{\mathbb{N}}"]                                               &  & {}                                                                  & \mathbb{N}                                             \\
                                                                                       &  &                                                                     &                                                        \\
\mathbb{B}^n \arrow[rrr, "\times_{\mathbb{B}^n}"] \arrow[uu, "\llbracket \cdot \rrbracket"] &  & {} \arrow[uu, "\llbracket \cdot \rrbracket", dotted, shift left=6] & \mathbb{B}^n \arrow[uu, "\llbracket \cdot \rrbracket"]
\end{tikzcd}
\caption{Specification of Multiplication}
\figlabel{comm}
\end{figure}
\end{frame}


\begin{frame}{Bit Multiplier}
  Our first building block is multiplication by a single bit.
  \pause The correctness specification is
  \[\forall b \in \mathbb{B}^{1} \quad A \in \mathbb{B}^{n} \qquad \llbracket b \times_{\mathbb{B}^{1,n}} A \rrbracket = \llbracket b \rrbracket \times_{N} \llbracket A \rrbracket\]
  \pause
  One implementation is
\begin{align*}\label{eq:mulbita}
  &\cdot \times_{\mathbb{B}^{1,m}} \cdot : \mathbb{B}^{1} \times \mathbb{B}^{n} \to \mathbb{B}^{n}\\
  &a \times_{\mathbb{B}^{1,m}} B =  if(a,B,0)
\end{align*}


\end{frame}


\begin{frame}{Shift Right}
  We also need the ability to double a number, which we will call $\cdot \ll 1$.
  \pause We will have specification
  \[\forall B \in \mathbb{B}^{n} \qquad \llbracket B \ll 1 \rrbracket = 2\llbracket B \rrbracket\]
  \pause We can implement the specification by just appending a $0$ to the end.

  \[b_{n-1}\cdots b_{1}b_{0} \ll 1 = b_{n-1}\cdots b_{1} b_{0} 0\]
\end{frame}

\begin{frame}{Shift and Add}
\begin{table}
  \begin{tabular}{c|c|c|c|c|c|c|c}
    &  & & & 1 & 0 & 1 & 1 \\
    &  & & $\times$ & 1 & 1 & 1 & 0 \\
    \hline

    &  & & & 0 & 0 & 0 & 0 \\
    &  & & 1 & 0 & 1 & 1 &  \\
     & & 1 & 0 & 1 & 1 & &   \\
      + & 1 & 0 & 1 & 1 &    \\
    \hline

      1 & 0 & 0 & 1 & 1 & 0 & 1 & 0    \\
\end{tabular}
\centering
\caption{An Example shift-and-add multiplication}
\label{tab:mul}
\end{table}

\begin{equation}\label{equation:addnshift}
  b_{n-1}\ldots b_{1}b_{0} \times_{\mathbb{B}^{n, m}} A = b_{0}\times_{\mathbb{B}^{1,m}} A + (b_{n-1}, \ldots, b_{1} \times_{\mathbb{B}^{n-1, m}} A) \ll 1
\end{equation}


\end{frame}


\begin{frame}{Future Work}
  \begin{enumerate}
    \item Carry-Lookahead Adders
    \pause \item Binary Subtraction
    \item Binary Division
\end{enumerate}
\end{frame}

\begin{frame}{Key Takeaways}
  \begin{enumerate}
    \pause \item We can formally prove the correctness of software and hardware components.
    \pause \item Homomoprhisms and category theory can give us more elegant and precise specifications.
\end{enumerate}
\end{frame}
\begin{frame}{Questions?}
  Ask me any questions.
  Or if you have any questions later
  \begin{enumerate}
    \item Email me at atticusmkuhn@gmail.com
     \item On Discord at Euler\#2074
\end{enumerate}
\end{frame}
\end{document}