Bump to unstable

.gitignore

@@ -6,5 +6,7 @@
 *.synctex.gz
 *.swp
 *.pdf
+*.vrb
 
 .DS_Store
+/result

DogeConfPBT/DogeConfPBT.tex

@@ -0,0 +1,993 @@
+\documentclass{beamer}
+\usepackage{listings}
+\usepackage{amsmath}
+\usepackage{caption}
+\usepackage{fancyvrb}
+\usepackage{xcolor}
+\usepackage{eso-pic}
+
+% Reproducible builds
+\pdfinfoomitdate=1
+\pdftrailerid{}
+\pdfsuppressptexinfo=-1
+
+\usepackage{color}
+\definecolor{bluekeywords}{rgb}{0.13,0.13,1}
+\definecolor{greencomments}{rgb}{0,0.5,0}
+\definecolor{turqusnumbers}{rgb}{0.17,0.57,0.69}
+\definecolor{redstrings}{rgb}{0.5,0,0}
+\definecolor{doge}{RGB}{240,218,149}
+\definecolor{lightdoge}{RGB}{245,228,169}
+\definecolor{grey}{RGB}{186,171,169}
+
+\setbeamercolor{background canvas}{bg=doge}
+\setbeamercolor{frametitle}{bg=lightdoge,fg=black}
+\setbeamercolor{section number projected}{bg=doge,fg=black}
+\setbeamercolor{section in toc shaded}{bg=doge, fg=grey}
+\setbeamercolor{subsection in toc shaded}{bg=doge, fg=grey}
+\useinnertheme{rectangles}
+\useoutertheme{shadow}
+
+\newcommand\AtPagemyUpperLeft[1]{\AtPageLowerLeft{%
+\put(\LenToUnit{0.9\paperwidth},\LenToUnit{0.88\paperheight}){#1}}}
+\AddToShipoutPictureFG{
+  \AtPagemyUpperLeft{{\includegraphics[width=1cm,keepaspectratio]{BabyDoge.png}}}
+}%
+
+\lstdefinelanguage{FSharp}
+    {morekeywords={val, let, new, match, with, rec, open, module, namespace, type, of, member, and, for, in, do, begin, end, fun, function, try, mutable, if, then, else},
+     keywordstyle=\color{bluekeywords},
+     sensitive=false,
+     morecomment=[l][\color{greencomments}]{///},
+     morecomment=[l][\color{greencomments}]{//},
+     morecomment=[s][\color{greencomments}]{{(*}{*)}},
+     morestring=[b]",
+     stringstyle=\color{redstrings}
+     }
+
+\title{Property-Based Testing}
+\author{Patrick Stevens}
+\institute{G-Research}
+\date{Doge Conf 2019}
+
+\lstnewenvironment{fslisting}
+  {
+    \lstset{
+        language=FSharp,
+        basicstyle=\small\ttfamily,
+        breaklines=true,
+        columns=fullflexible}
+  }
+  {
+  }
+
+\begin{document}
+
+\begin{frame}
+\titlepage
+\end{frame}
+
+\section{What's the problem?}
+\subsection{A program to test}
+
+\begin{frame}
+\tableofcontents
+\end{frame}
+
+\begin{frame}
+\tableofcontents[currentsection]
+\end{frame}
+
+\begin{frame}
+\frametitle{Let's have something to test}
+Interval set: a space-efficient set of integers
+
+Defining example:
+$$\{{\color{red}1,2,3,4},{\color{cyan}8,9,10}\}$$ $$[{\color{red}(1, 4)}, {\color{cyan}(8, 10)}]$$
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Public API}
+\begin{fslisting}
+type IntervalSet
+
+[<RequireQualifiedAccess>]
+module IntervalSet =
+    val empty : IntervalSet
+    val add : int -> IntervalSet -> IntervalSet
+    val contains : int -> IntervalSet -> bool
+\end{fslisting}
+
+\end{frame}
+
+\begin{frame}
+\frametitle{Implementation}
+This is a presentation about testing.
+
+Yes, there will be a bug somewhere.
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Data structure}
+
+\begin{fslisting}
+type private Interval =
+    {
+        Min : int
+        Max : int
+    }
+
+type IntervalSet = private IntervalSet of Interval list
+
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: empty}
+
+\begin{fslisting}
+[<RequireQualifiedAccess>]
+module IntervalSet =
+    let empty = IntervalSet []
+
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: insertion}
+\begin{fslisting}
+let private rec add' (a : int) (ls : Interval list) =
+    match ls with
+    | [] -> [{ Min = a ; Max = a }]
+    | _ -> ...
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: insertion}
+\begin{fslisting}
+let private rec add' (a : int) (ls : Interval list) =
+    match ls with
+    | [] -> ...
+    | interval :: is ->
+        if interval.Min <= a && a <= interval.Max then
+            ls // no need to add, it's already there
+        else ...
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: insertion}
+\begin{fslisting}
+let private rec add' (a : int) (ls : Interval list) =
+    match ls with
+    | [] -> ...
+    | interval :: is ->
+        if // already there...
+        elif interval.Min - 1 = a then
+            { interval with Min = interval.Min - 1 }
+            :: is // augment this interval to contain a
+        elif interval.Max + 1 = a then
+            { interval with Max = interval.Max + 1 }
+            :: is // augment this interval to contain a
+        ...
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: insertion}
+\begin{fslisting}
+let private rec add' (a : int) (ls : Interval list) =
+    match ls with
+    | [] -> ...
+    | interval :: is ->
+        if // already there...
+        elif // can be added to this interval...
+        else // can't add it here; recurse
+            add' a is
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: insertion}
+\begin{fslisting}
+[<RequireQualifiedAccess>]
+module IntervalSet =
+    let add (a : int) (IntervalSet intervals) =
+        add' a intervals
+        |> IntervalSet
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Implementation: containment}
+
+\begin{fslisting}
+let rec contains (a : int) (IntervalSet ls) =
+    ls
+    |> List.tryFind (fun interval ->
+        interval.Min <= a && a <= interval.Max)
+    |> Option.isSome
+\end{fslisting}
+\end{frame}
+
+\subsection{Testing the program}
+
+\begin{frame}[fragile]
+\frametitle{Start testing!}
+Helper function for tests:
+\begin{fslisting}
+let create (is : int list) : IntervalSet =
+    is
+    |> List.fold
+        (fun set i -> IntervalSet.add i set)
+        IntervalSet.empty
+\end{fslisting}
+\end{frame}
+\begin{frame}
+\frametitle{What can we test?}
+We should test some different lists and their resulting IntervalSets.
+
+\begin{itemize}
+    \item $[3; 4]$ contains $5$? (No.)
+    \item $[3; 5]$ contains $5$? (Yes.)
+    \item $[3; 4; 5]$ contains $4$? (Yes.)
+\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{The test cases}
+\begin{fslisting}
+    create [3; 4]
+    |> IntervalSet.contains 5
+    |> shouldEqual false
+
+    create [3; 5]
+    |> IntervalSet.contains 5
+    |> shouldEqual true
+
+    create [3; 4; 5]
+    |> IntervalSet.contains 4
+    |> shouldEqual true
+\end{fslisting}
+\pause
+Hooray, the tests pass!
+\end{frame}
+
+\subsection{But can I really trust myself?}
+
+\begin{frame}
+\frametitle{... but is it right?}
+\end{frame}
+
+\begin{frame}
+\frametitle{... but is it right?}
+
+I don't know!
+
+\begin{itemize}
+\item I'm lazy
+\item I'm stupid
+\item I hate testing
+\end{itemize}
+
+Isn't there a better way?
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{FsCheck can help!}
+
+Sneak peek: FsCheck will tell us that this implementation is wrong.
+
+\begin{Verbatim}[commandchars=\\\{\}]
+\textcolor{red}{Falsifiable}, after 35 tests (15 shrinks)
+  (StGen 9514417537,296661223)):
+Original:
+[0; 0; 0; 0; 0; 0; 0; 12; 1; -2; 0; 0; 0; 0; 0; 0; 0]
+12
+Shrunk:
+[12; 0]
+12
+\end{Verbatim}
+
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{FsCheck's test}
+The last two lines FsCheck gave us were:
+\begin{verbatim}
+[12; 0]
+12
+\end{verbatim}
+
+\pause
+
+FsCheck found this test:
+
+\begin{fslisting}
+create [12; 0]
+|> IntervalSet.contains 12
+|> shouldEqual true
+\end{fslisting}
+\end{frame}
+
+\section{Introduction to FsCheck}
+\subsection{FsCheck's view of the world}
+
+\begin{frame}
+\tableofcontents[currentsection]
+\end{frame}
+
+\begin{frame}
+\frametitle{Why do you test?}
+
+\begin{itemize}
+    \item Your program does what you want it to.
+    \item Your program doesn't do what you don't want it to.
+\end{itemize}
+\end{frame}
+
+\begin{frame}
+\frametitle{How do you normally test?}
+
+\begin{enumerate}
+    \item Come up with examples.
+    \item Work out what your program should do on those examples.
+    \item Run the program and check it did what you wanted.
+\end{enumerate}
+\end{frame}
+
+\begin{frame}
+\frametitle{But what are you \emph{really} doing?}
+
+You're testing \emph{properties} through \emph{representative examples}.
+\end{frame}
+
+\begin{frame}
+    Why not just \emph{test properties}?
+\end{frame}
+
+\begin{frame}
+\frametitle{FsCheck tests properties automatically}
+
+\begin{itemize}
+    \item Find edge cases
+    \item Find large, complicated cases
+    \item Shrink large cases automatically
+    \item Make sure you can repeat any failures (the TDD way!)
+\end{itemize}
+\end{frame}
+
+\subsection{Back to the example}
+
+\begin{frame}
+\frametitle{The failing property for IntervalSet}
+\begin{itemize}
+\item Create an IntervalSet from a list of integers\dots
+\item then check for containment\dots
+\item should be the same as checking the original list.
+\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{The failing property for IntervalSet, in code}
+\begin{fslisting}
+let property (ints : int list) (toCheck : int) : bool =
+    create ints
+    |> IntervalSet.contains toCheck
+    |> (=) (List.contains doesContain ints)
+\end{fslisting}
+
+% Remember, FsCheck told us that this property failed.
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Invoke FsCheck}
+\begin{fslisting}
+open FsCheck
+
+let property (ints : int list) (toCheck : int) : bool =
+    create ints
+    |> IntervalSet.contains toCheck
+    |> (=) (List.contains doesContain ints)
+
+[<Test>]
+let testProperty () =
+    Check.QuickThrowOnFailure property
+\end{fslisting}
+
+% Remember, FsCheck told us that this failed.
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{FsCheck's output, revisited}
+\begin{Verbatim}[commandchars=\\\{\}]
+Falsifiable, after \textcolor{red}{35} tests (15 shrinks)
+  (StGen 9514417537,296661223)):
+Original:
+[0; 0; 0; 0; 0; 0; 0; 12; 1; -2; 0; 0; 0; 0; 0; 0; 0]
+12
+Shrunk:
+\textcolor{cyan}{[12; 0]}
+\textcolor{cyan}{12}
+\end{Verbatim}
+
+\hfill \break
+
+FsCheck constructed \textcolor{red}{35} tests before finding a failure.
+It then shrank the test case to \textcolor{cyan}{the smallest failure} it could find.
+\end{frame}
+
+\subsection{Advantages}
+
+\begin{frame}
+\frametitle{Advantages}
+
+\begin{itemize}
+\item No thought required!
+\item Perfectly reproducible
+\item Edge cases automatically examined closely
+\item Randomised testing increases coverage
+\end{itemize}
+
+\hfill \break
+
+(Make sure you explicitly test any failures FsCheck finds, so that nothing is lost to the mists of time!)
+\end{frame}
+
+\subsection{What was the bug?}
+\begin{frame}[fragile]
+\frametitle{The bug}
+\begin{fslisting}
+let private rec add' (a : int) (ls : Interval list) =
+    match ls with
+    | [] -> [{ Min = a ; Max = a }]
+    | interval :: is ->
+        if (* contains *) then
+            ls
+        elif (* is 1 below *) then
+        elif (* is 1 above *) then
+        else
+            add' a is // <-- Oh no!
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{The fix}
+\begin{fslisting}
+let private rec add' (a : int) (ls : Interval list) =
+    match ls with
+    | [] -> [{ Min = a ; Max = a }]
+    | interval :: is ->
+        if (* contains *) then
+            ls
+        elif (* is 1 below *) then
+        elif (* is 1 above *) then
+        else
+            interval :: add' a is
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{FsCheck is happy}
+\begin{verbatim}
+Ok, passed 100 tests.
+\end{verbatim}
+\end{frame}
+
+\subsection{Serialisers}
+\begin{frame}
+\frametitle{Serialisers: the hello-world of black-box testing}
+
+A serialiser is defined by a property:
+
+\hfill \break
+
+\noindent\fbox{%
+Writing an object, then reading it in, gives the original object.
+}
+
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Signature of a serialiser}
+
+\begin{fslisting}
+[<RequireQualifiedAccess>]
+module FancyThing =
+    val toString : FancyThing -> string
+    val parse : string -> FancyThing option
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Test the serialiser}
+
+\begin{fslisting}
+[<Test>]
+let roundTripTest () =
+    let property (t : FancyThing) : bool =
+        t
+        |> FancyThing.toString
+        |> FancyThing.parse
+        |> (=) (Some t)
+    Check.QuickThrowOnFailure property
+\end{fslisting}
+\end{frame}
+
+\begin{frame}
+\frametitle{What FsCheck gave us}
+Without needing to know anything about the implementation, FsCheck was still able to produce useful tests!
+\end{frame}
+
+\section{Metatesting}
+\tableofcontents[currentsection]
+
+\begin{frame}
+\frametitle{Metatesting}
+A technique you should use to make your testing more effective.
+\end{frame}
+
+\subsection{Was the testing comprehensive?}
+
+\begin{frame}[fragile]
+\frametitle{How can we be sure we tested enough?}
+
+Recall the property:
+\begin{fslisting}
+let property (ints : int list) (toCheck : int) : bool =
+    create ints
+    |> IntervalSet.contains toCheck
+    |> (=) (List.contains doesContain ints)
+
+\end{fslisting}
+
+\pause
+By fluke (or my incompetence), FsCheck might never generate a ``yes, does contain'' case.
+\end{frame}
+
+\begin{frame}
+\frametitle{Gather metrics}
+F\# is impure and side-effectful, so it's extremely easy to gather metrics.
+
+\hfill \break
+
+(Instrumentation is an example where purity really does make things harder!)
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Gather metrics in the property}
+\begin{fslisting}
+let property
+    (positives : int ref) (negatives : int ref)
+    (ints : int list)
+    (toCheck : int)
+    : bool
+    =
+    let contains = List.contains doesContain ints
+    if contains then
+        incr positives
+    else
+        incr negatives
+
+    create ints
+    |> IntervalSet.contains toCheck
+    |> (=) contains
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Invoke the augmented test}
+\begin{fslisting}
+[<Test>]
+let test () =
+    let pos = ref 0
+    let neg = ref 0
+    Check.QuickThrowOnFailure (property pos neg)
+
+    let pos = pos.Value
+    let neg = neg.Value
+
+    pos |> shouldBeGreaterThan 0
+    neg |> shouldBeGreaterThan 0
+
+    (float pos) / (float pos + float neg)
+    |> shouldBeGreaterThan 0.1
+\end{fslisting}
+\end{frame}
+
+\begin{frame}
+At least a tenth of the time, we want to be hitting positive cases, but \dots
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{The test is a bit unreliable!}
+\begin{verbatim}
+Expected: 0.1
+Actual: 0.08
+
+at FsUnitTyped.TopLevelOperators.shouldBeGreaterThan
+\end{verbatim}
+\end{frame}
+
+\subsection{Manipulating the cases}
+\begin{frame}
+\frametitle{Manipulating the generated cases}
+We want to generate cases that aren't so often ``look for something that's not in the list''.
+
+FsCheck gives us access to its \emph{generators} for this purpose.
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Generators}
+We will have the property remain the same, but tell FsCheck to generate different cases.
+
+FsCheck has a number of built-in generators.
+It also has a computation expression to manipulate generators.
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Generator of bounded integers}
+
+\begin{fslisting}
+let someInts : Gen<int> = Gen.choose (-100, 100)
+Gen.sample 0 5 someInts
+// output: [57; -24; 67; -14; 77]
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Generator of bounded even integers}
+\begin{fslisting}
+let someInts : Gen<int> = Gen.choose (-100, 100)
+let evenIntegers : Gen<int> = gen {
+    let! (anyInt : int) = someInt
+    return 2 * anyInt
+}
+Gen.sample 0 5 someInts
+// output: [-190; -24; -194; -108; -112]
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Size}
+\begin{fslisting}
+let integers : Gen<int list> =
+    Gen.sized (fun i ->
+        Gen.choose (-100, 100)
+        |> Gen.listOfLength i)
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Generator that sometimes selects from a list}
+\begin{fslisting}
+let integers : Gen<int list> = ...
+
+let listAndElt : Gen<int * int list> = gen {
+    let! (list : int list) = integers
+\end{fslisting}
+\pause
+\begin{fslisting}
+    let genFromList = Gen.elements list
+\end{fslisting}
+\pause
+\begin{fslisting}
+    let genNotFromList =
+        Gen.choose (-100, 100)
+        |> Gen.filter (fun i -> not (List.contains i list))
+\end{fslisting}
+\pause
+\begin{fslisting}
+    let! number = Gen.oneOf [genFromList ; genNotFromList]
+    return (number, list)
+}
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Using this generator}
+
+The generator makes pairs of an integer and a list, where the integer is 50\% likely to appear in the list.
+
+\begin{fslisting}
+[<Test>]
+let test () =
+    let (pos, neg) = (ref 0), (ref 0)
+
+    (fun (list, elt) -> property pos neg elt list)
+    |> Prop.forAll (Arb.fromGen listAndElt)
+    |> Check.QuickThrowOnFailure
+
+    let pos = pos.Value |> float
+    let neg = neg.Value |> float
+
+    pos / (pos + neg)
+    |> shouldBeGreaterThan 0.1
+\end{fslisting}
+\end{frame}
+
+\begin{frame}[fragile]
+\begin{verbatim}
+Ok, passed 100 tests.
+\end{verbatim}
+
+In fact we now have a positive case about 50\% of the time.
+\end{frame}
+
+\section{Stateful systems}
+
+\begin{frame}
+\tableofcontents[currentsection]
+\end{frame}
+
+\begin{frame}
+\frametitle{Stateful systems}
+What about state?
+
+Key idea: \emph{describe what to do}, and then do it.
+\end{frame}
+
+\subsection{Example}
+\begin{frame}[fragile]
+\frametitle{Example: a stream}
+Simple model: array and pointer.
+
+\begin{table}
+\captionsetup{labelformat=empty}
+\caption{Starting state, pointer at index $0$}
+\begin{tabular}{ |c|c|c|c|c|c|c|c }
+    \hline
+    \color{red}72 & 69 & 76 & 76 & 79 & 32 & 87 & \dots \\
+    \hline
+\end{tabular}
+\end{table}
+
+\begin{table}
+\captionsetup{labelformat=empty}
+\caption{Seek to index $2$}
+\begin{tabular}{ |c|c|c|c|c|c|c|c }
+    \hline
+    72 & 69 & \color{red}76 & 76 & 79 & 32 & 87 & \dots \\
+    \hline
+\end{tabular}
+\end{table}
+
+\begin{table}
+\captionsetup{labelformat=empty}
+\caption{Write $88$ at the current index}
+\begin{tabular}{ |c|c|c|c|c|c|c|c }
+    \hline
+    72 & 69 & \color{red}88 & 76 & 79 & 32 & 87 & \dots \\
+    \hline
+\end{tabular}
+\end{table}
+
+\end{frame}
+
+\begin{frame}[fragile]
+Imagine we can't access the implementation, but we want to test it anyway.
+
+\begin{fslisting}
+type Stream
+
+[<RequireQualifiedAccess>]
+module Stream =
+    val uninitialised : unit -> Stream
+
+    val read : Stream -> byte
+    val write : Stream -> byte -> unit
+    val seek : Stream -> int -> unit
+    val currentIndex : Stream -> int
+\end{fslisting}
+\end{frame}
+
+\begin{frame}
+\frametitle{Some things to test}
+\begin{itemize}
+    \item Write then read
+    \item Seek then get index
+    \item Write, seek away, seek back, read
+\end{itemize}
+
+\hfill \break
+FsCheck will do these, and do them well, but they are all quite specific.
+
+Isn't the point of FsCheck to take this drudgery away from us?
+\end{frame}
+
+\begin{frame}
+\frametitle{Obstacles to FsCheck}
+
+Why is FsCheck not helping here?
+
+\begin{itemize}
+    \item Testing a mutable object
+    \item No obvious immutable model to use
+    \item How to generate random streams?
+    \item Need shrinking not to interfere with itself
+\end{itemize}
+\end{frame}
+
+\begin{frame}
+Answer: \emph{describe} what to do, and \emph{then} do it!
+
+\pause
+\hfill \break
+
+\tiny{c.f. initial algebras}
+
+\end{frame}
+
+\subsection{Testing with FsCheck}
+
+\begin{frame}[fragile]
+\frametitle{Domain model}
+\begin{fslisting}
+type StreamInteraction =
+| Write of byte
+| Read
+| Seek of int
+| CurrentIndex
+
+type TestCase = StreamInteraction list
+\end{fslisting}
+
+\end{frame}
+\begin{frame}[fragile]
+\begin{fslisting}
+[<RequireQualifiedAccess>]
+module TestCase =
+    let rec prepareStream
+        (s : Stream)
+        (instructions : TestCase)
+        =
+        for instruction in instructions do
+            match instructions with
+            | Write b ->
+                Stream.write s b
+            | Read ->
+                Stream.read s |> ignore
+            | Seek n ->
+                Stream.seek s n
+            | CurrentIndex ->
+                Stream.currentIndex s |> ignore
+
+\end{fslisting}
+\end{frame}
+
+\begin{frame}
+\frametitle{Suddenly an immutable model appeared!}
+
+\begin{itemize}
+\item By constructing test cases through their \emph{descriptions}\dots
+\item we made an immutable model of the world.
+\item FsCheck can generate these things completely automatically!
+\end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+\frametitle{Immediately useful...}
+This can be used with no further modification to check a very useful property:
+
+\begin{fslisting}
+[<Test>]
+let doesNotCrash () =
+    let property (instructions : StreamInteraction list) =
+        let s = Stream.uninitialised ()
+        TestCase.prepareStream s instructions
+        true
+
+    Check.QuickThrowOnFailure (property)
+\end{fslisting}
+\end{frame}
+
+\begin{frame}
+\frametitle{... and more useful with generalisation}
+But it really shines with just a little more work.
+\end{frame}
+
+\begin{frame}
+\frametitle{The index only changes when you expect it to}
+\begin{enumerate}
+\item Make a generator for all interactions that shouldn't modify the index
+\item Generate a list of interactions
+\item Generate a list of interactions which don't modify the index
+\item Concatenate
+\item Execute, and assert that the index hasn't changed.
+\end{enumerate}
+\end{frame}
+
+\begin{frame}
+\frametitle{The gold standard: an immutable model}
+
+\begin{enumerate}
+\item Define a map of ``index'' to ``current value''
+\item Interpret the interactions as acting on that map
+\item Generate a list of interactions
+\item Verify that the accessible output from the stream is indistinguishable from the output of the map.
+\end{enumerate}
+\end{frame}
+
+\begin{frame}
+\frametitle{Aside: model-based testing}
+
+This has a name: \emph{model-based testing}.
+
+\hfill \break
+
+\noindent\fbox{%
+Checking behaviour relative to a more easily specified model.
+}
+
+\hfill \break
+
+MBT is a subset of property-based testing.
+
+The property is ``the system behaves like the model does''.
+
+(Contrast: serialiser. Correctness defined by property, not model.)
+
+\hfill \break
+
+FsCheck also has dedicated built-in support for MBT.
+\end{frame}
+
+\begin{frame}
+\frametitle{Sketch: Testing a UI}
+Test a UI by\dots
+\begin{enumerate}
+    \item Identifying the actions you want to test;
+    \item Generating lists of actions;
+    \item Applying the actions;
+    \item Checking the final state is as expected given the actions.
+\end{enumerate}
+\end{frame}
+
+\begin{frame}
+\frametitle{Small properties, incremental addition}
+
+The UI example is good:
+\begin{itemize}
+\item Enormous space of possible actions
+\item Some actions very hard to test?
+\item Don't care uniformly about correctness
+\end{itemize}
+
+\hfill \break
+
+Don't need to test everything!
+\end{frame}
+
+\begin{frame}
+\frametitle{A restricted search space}
+
+If you're struggling to find properties, restrict the search space!
+
+If you're struggling to define correctness, restrict the search space!
+
+\hfill \break
+
+Cut down to a small subset of user interactions, and you will find properties.
+\end{frame}
+
+\begin{frame}
+\frametitle{Doge Analytics}
+
+(Here is where I waffle, because these slides are on public Github)
+\end{frame}
+
+\section*{Summary}
+\begin{frame}
+\frametitle{Why you should use PBT}
+Property-based testing...
+\begin{itemize}
+\item is easy
+\item exists in many languages (Python, F\#, Haskell, \dots)
+\item can be added incrementally
+\item is as comprehensive as you want
+\item tests anything (black-box or otherwise)
+\end{itemize}
+\end{frame}
+
+\end{document}

Tennenbaum/Tennenbaum.tex

@@ -157,4 +157,4 @@ This contradicts the undecidability of $X$.
 \section{Acknowledgements}
 The structure of the proof is from Dr Thomas Forster's lecture notes on Computability and Logic from Part III of the Cambridge Maths Tripos, lectured in 2016.
 
-\end{document}
+\end{document}

YonedaWithoutTears/YonedaWithoutTears.tex

@@ -55,7 +55,7 @@
     \begin{definition}
         Let $F, G: \mathcal{C} \to \mathcal{D}$ be functors.
         A \emph{natural transformation} from $F$ to $G$ is a selection $\alpha$, parametrised over each $X \in \mathcal{C}$, of an arrow $\alpha_X$ in $\mathcal{D}$ from $FX \to GX$.
-        We require this selection to be ``natural'' in that whenever $f : X \to Y$ is an arrow in $\mathcal{C}$, we have $$FX \xrightarrow{Ff} FY \xrightarrow{\alpha_Y} GY = FX \xrightarrow{\alpha_X} GX \xrightarrow{Gf} GY$$
+        We require this selection to be ``natural'' in that whenever $f : X \to Y$ is an arrow in $\mathcal{C}$, we have $$(FX \xrightarrow{Ff} FY \xrightarrow{\alpha_Y} GY) = (FX \xrightarrow{\alpha_X} GX \xrightarrow{Gf} GY)$$
     \end{definition}
 
     \
@@ -74,7 +74,7 @@
     \begin{thm}[The Yoneda lemma]
         Let $\mathcal{C}$ be a category, and let $G: \mathcal{C} \to \Set$ be a functor.
         Let $A$ be an object of $\mathcal{C}$.
-        Then $$\Nat [\homfrom{A} \to G ] \cong G A$$
+        Then $$\Nat [\homfrom{A}, G] \cong G A$$
         and moreover the bijection is natural in both $G$ and $A$.
     \end{thm}
 
@@ -121,7 +121,7 @@
     (Note that this is not quite what is usually meant by a model homomorphism, and I have invented the term ``fixed model homomorphism'' to describe it.)
     
     A \emph{fixed model homomorphism} $\alpha$ is a function from one model $F: \mathcal{C} \to \Set$ of the theory $\mathcal{C}$ to another model $G: \mathcal{C} \to \Set$, which assigns to each type $FA$ of the model $F$ the corresponding type $GA$ of the model $G$, in such a way that $\alpha$ respects the predicates $Ff: FA \to FB$ of the model:
-    $$FA \xrightarrow{Ff} FB \xrightarrow{\alpha_B} GB = FA \xrightarrow{\alpha_A} GA \xrightarrow{Gf} GB$$
+    $$(FA \xrightarrow{Ff} FB \xrightarrow{\alpha_B} GB) = (FA \xrightarrow{\alpha_A} GA \xrightarrow{Gf}) GB$$
 
 Notice that this is a model homomorphism which additionally ensures that $FA$ is always mapped to $GA$ (for any $A$), so (for example) it won't collapse all the objects $FA$ into a single object in $G$'s image unless $G$ is the trivial model.
 
@@ -130,7 +130,7 @@ Notice that this is a model homomorphism which additionally ensures that $FA$ is
     So the second key insight is that a natural transformation between functors $F: \mathcal{C} \to \Set$ and $G$ is just a fixed homomorphism between the $\Set$-models $F$ and $G$ of the theory $\mathcal{C}$.
 
     \section{Free models}
-    Throughout mathematics, there is the notion of a free object: an object which somehow has the least possible structure while still obeying all the rules it has to obey.
+    Throughout mathematics, there is the notion of a free object: an object which somehow has the least possible restriction while still obeying all the rules it has to obey.
     Can we find a free model of the theory represented by the category $\mathcal{C}$?
 
     Imagine $\mathcal{C}$ has two objects. Then any free model worth its name must have at least two types - otherwise we've definitely lost information in the model.
@@ -253,4 +253,4 @@ I'm afraid I don't know of a good way to think about naturality other than just
     This entire document is derived from an answer by Sridhar Ramesh on a Math Overflow answer at \url{https://mathoverflow.net/a/15143}.
 
 
-\end{document}
+\end{document}

build.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+
+USER_DIR=$(readlink -f "$1")
+
+mkdir "output"
+
+# Build PDFs from LaTeX.
+find "$USER_DIR" -type f -name '*.tex' -print0 | while IFS= read -r -d '' file; do
+  output=$(readlink -f "$(dirname "$file")/$(basename "$file" .tex).pdf")
+  if [ -f "$output" ]; then
+      echo "Skipping $file as already built"
+  else
+      file=$(readlink -f "$file")
+      echo "$file - $output"
+      pushd "$(dirname "$output")" || exit 1
+      # Do the build twice to sort out any bookmarks.
+      HOME=$(pwd) SOURCE_DATE_EPOCH=1622905527 pdflatex "$file" || exit 1
+      HOME=$(pwd) SOURCE_DATE_EPOCH=1622905527 pdflatex "$file" || exit 1
+      popd || exit 1
+  fi
+done
+
+cd "$USER_DIR" || exit 1

flake.lock

@@ -0,0 +1,77 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1725634671,
+        "narHash": "sha256-v3rIhsJBOMLR8e/RNWxr828tB+WywYIoajrZKFM+0Gg=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "574d1eac1c200690e27b8eb4e24887f8df7ac27c",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs",
+        "scripts": "scripts"
+      }
+    },
+    "scripts": {
+      "locked": {
+        "lastModified": 1696031019,
+        "narHash": "sha256-MuKEC8ZZ1Znm2idxQEQYU18z/1l9rjBZaj5gdKd9elQ=",
+        "owner": "Smaug123",
+        "repo": "flake-shell-script",
+        "rev": "05cc0582a193d3b42b6b4e64c6ec7a9bca4bb3c5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "Smaug123",
+        "repo": "flake-shell-script",
+        "type": "github"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,48 @@
+{
+  description = "PDFs hosted on patrickstevens.co.uk";
+
+  inputs = {
+    flake-utils.url = "github:numtide/flake-utils";
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+    scripts.url = "github:Smaug123/flake-shell-script";
+  };
+
+  outputs = {
+    self,
+    nixpkgs,
+    flake-utils,
+    scripts,
+  }: let
+    commit = self.shortRev or "dirty";
+    date = self.lastModifiedDate or self.lastModified or "19700101";
+    version = "1.0.0+${builtins.substring 0 8 date}.${commit}";
+  in
+    flake-utils.lib.eachDefaultSystem (system: let
+      pkgs = nixpkgs.legacyPackages.${system};
+    in let
+      texlive = pkgs.texlive.combine {
+        inherit (pkgs.texlive) scheme-basic mdframed etoolbox zref needspace tikz-cd mathtools metafont pgf beamer listings caption fancyvrb eso-pic;
+      };
+    in {
+      packages.default = pkgs.stdenv.mkDerivation {
+        __contentAddressed = true;
+        inherit version;
+        pname = "patrickstevens.co.uk-pdfs";
+        src = ./.;
+        buildInputs = [texlive];
+        buildPhase = ''
+          ${pkgs.bash}/bin/sh ${scripts.lib.createShellScript pkgs "latex" ./build.sh}/run.sh .
+        '';
+
+        installPhase = ''
+          mkdir -p $out
+          cp ./**/*.pdf $out
+          cp ./**/*.tex $out
+          cp ./pdf-targets.txt $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [pkgs.alejandra pkgs.shellcheck texlive];
+      };
+    });
+}

pdf-targets.txt

@@ -9,4 +9,4 @@ static/misc/TokyoEntrance2016/TokyoEntrance2016.tex
 static/misc/NonstandardAnalysis/NonstandardAnalysisPartIII.tex
 static/misc/RepresentableFunctors/RepresentableFunctors.tex
 static/misc/YonedaWithoutTears/YonedaWithoutTears.tex
-
+static/misc/DogeConfPBT/DogeConfPBT.tex