docs(course): add motivation for each chapter

doc/advanced-testing-mini-course/README.md

@@ -45,7 +45,16 @@
 
 ### 1. State machine testing
 
-* The software under test (SUT)
+* Motivation
+
+  - Testing: "the process of using or trying something to see if it works, is
+    suitable, obeys the rules, etc." -- Cambridge dictionary
+
+  - In order to check that the software under test (SUT) obeys the rules we must
+    first write the rules down
+
+  - State machine specifications are one of many ways to formally "write down
+    the rules"
 
 ```haskell
 newtype Counter = Counter (IORef Int)
@@ -83,22 +92,96 @@ step m cmd = case cmd of
 exec :: Counter -> Command -> IO Response
 exec = undefined
 
-genCommands :: Model -> Gen [Command]
-genCommands = undefined
+newtype Program = Program [Command]
+
+genProgram :: Model -> Gen Program
+genProgram = undefined
 
 prop_counter :: Property
-prop_counter = forAll genCommands $ \cmds -> do
+prop_counter = forAll genProgram $ \(Program cmds) -> do
   undefined
 ```
 
+* Excerises
+
+1. Implement shrinking for programs.
+
+2. Collect timing information about how long each command takes to execute on
+   average.
+
+* See also
+
+  - Why state machines over other forms of specifications?
+    + Executable (we will use this later)
+    + Gurevich's generalisation of the Church-Turing thesis
+    + Already heavily used in distributed systems
+
 ### 2. Concurrent state machine testing with linearisability
 
+* Motivation
+
+  - In the previous chapter we saw how to test if a sequential (single-threaded)
+    program respects some state machine specification
+
+  - Next we show how the *same* specification can be used to check if a
+    concurrent execution is correct using linearisability
+
+  - E.g. counters are often shared among different threads, how can we test that
+    the counter implementation is thread-safe?
+
+```haskell
+newtype Program = Program [Command]
+
+newtype ConcProgram = ConcProgram [[Command]]
+
+genConcProgram :: Model -> Gen ConcProgram
+genConcProgram = undefined
+
+validConcProgram :: Model -> Precondition -> ConcProgram -> Bool
+validConcProgram = undefined
+
+data History = History Op
+
+execConc :: ConcProgram -> IO History
+execConc = undefined
+
+linearisable :: History -> Bool
+linearisable = undefined
+```
+
 ### 3. Consumer-driven contract testing using state machines
 
+* Motivation
+
+  - Components rarely exist in isolation, they almost always depend on some
+    other component;
+
+  - When we test we often want to test as if the component existed in isolation,
+    e.g. if component A depends on component B, we'd like to test B first and
+    then *assume* that B is working when testing A;
+
+  - Assumptions like these can be justified using so called *contract tests*.
+
 ### 4. Fault-injection
 
+* Motivation
+  - "almost all (92%) of the catastrophic system failures are the result of
+    incorrect handling of non-fatal errors explicitly signaled in software.
+    [...] in 58% of the catastrophic failures, the underlying faults could
+    easily have been detected through simple testing of error handling code." --
+    [Simple Testing Can Prevent Most Critical Failures: An Analysis of
+    Production Failures in Distributed Data-intensive
+    Systems](http://www.eecg.toronto.edu/~yuan/papers/failure_analysis_osdi14.pdf)
+    (2014) Yuan et al;
+
 ### 5. Simulation testing
 
+* Motivation
+
+  - "haven't tested foundation[db] in part because their testing appears to be
+    waaaay more rigorous than mine." -- Kyle
+    ["aphyr"](https://twitter.com/aphyr/status/405017101804396546) Kingsbury
+
 ```haskell
 data Network = Network
   { deploy  :: Addr -> IO () -- bind and listen