content: = Ancient Greek computer science =
  
  To understand X, Socrates began by asking: "What is X?". For example:
  "What is justice?", or "What is virtue?"
  
  His interlocutor typically gave an impressive but imprecise definition, to
  which Socrates asked a series of follow-up questions. Sooner or later, he'd
  find a contradiction. Both parties gained a deeper understanding of the topic,
  but even after several iterations, the main conclusion most often seemed to be
  "X is hard to define". Awfully little to extract from such a long process.
  
  I first encountered an optimization in a book by Douglas Adams. Reply
  mathematically! When asked: "What is the answer to the meaning of life, the
  universe, and everything?", we say "42" and pre-empt those meddlesome
  contradictions. For if mathematics is flawed, then so is logical reasoning, and
  hence the Socratic method itself. Fight logic with logic. As Hilbert asked in
  his paper _On the infinite_: "And where else would reliability and truth be
  found if even mathematical thinking fails?"
  
  Now the problem is to find a mathematical definition that reflects what we have
  in mind. This can be difficult, but often in computer science, mathematical
  definitions work well, and even guide the implementation.
  
  == What is a compiler? ==
  
  We define a compiler to be a translator from one programming language to
  another. More mathematically, a compiler is a function that maps a program in
  the source language to a program in the target language:
  
  ------------------------------------------------------------------------
  compile :: Language -> TargetLanguage
  ------------------------------------------------------------------------
  
  But not just any function will do. A compiler must preserve the
  meaning of the source program.
  
  == What is a programming language? ==
  
  Running a program produces an output from an input, so we define a programming
  language by means of an interpreter, which takes a program to a function
  mapping input values to output values:
  
  ------------------------------------------------------------------------
  interpret :: Language -> (Value -> Value)
  interpretTarget :: TargetLanguage -> (Value -> Value)
  ------------------------------------------------------------------------
  
  By convention, the arrow `+(->)+` associates to the right, so we write:
  
  ------------------------------------------------------------------------
  interpret :: Language -> Value -> Value
  interpretTarget :: TargetLanguage -> Value -> Value
  ------------------------------------------------------------------------
  
  Our condition for a compiler correctness is that for any program `p` in
  `Language`, and for any `input` in `Value`:
  
  ------------------------------------------------------------------------
  (interpret p) input == (interpretTarget (compile p)) input
  ------------------------------------------------------------------------
  
  By convention, juxtaposition denotes function application and associates to the
  left, which plays nicely with our other convention, so we write:
  
  ------------------------------------------------------------------------
  interpret p input == interpretTarget (compile p) input
  ------------------------------------------------------------------------
  
  So far so good, but there ought to be some indication that these interpreters
  are running on computers.
  
  == What is a computer? ==
  
  We could leave it as is:
  
  ------------------------------------------------------------------------
  compute :: Value -> Value
  ------------------------------------------------------------------------
  
  This works if we say the input includes the entire state of the computer: every
  register, every single bit of memory, and so on. However, we've bitten off far
  more than we can chew; how can we reason about a complicated gigantic function?
  
  What if we shrink the domain and range?
  
  ------------------------------------------------------------------------
  compute :: Char -> Char
  ------------------------------------------------------------------------
  
  Here, the set `Char` is relatively small, say the set of all 32-bit words.
  
  A list of `Char` can hold inputs and outputs of arbitrary length:
  
  ------------------------------------------------------------------------
  type Value = [Char]
  ------------------------------------------------------------------------
  
  Unfortunately, all our `compute` function can do with such a list is to perform
  the same operation to each element of the list. We have modeled something like
  a circuit, which performs the same task on a fixed number of bits at a time.
  
  == Deterministic Finite Automata ==
  
  Humans and computers are more than mere circuits because we retain information
  from one step to use in future steps. Even though we can only read a few words
  at a time, we can absorb a complex story from a book. This is because after
  starting in one state of mind, processing a few bits can put us in another
  state of mind.
  
  This leads us to consider deterministic finite automata, or finite state
  machines:
  
  \begin{code}
  type State = Int
  type Dfa = (State, State -> Char -> State, State -> Bool)
  
  runDfa :: Dfa -> [Char] -> Bool
  runDfa (start, step, accepts) s = go start s where
    go state s = case s of
      ""     -> accepts state
      c:rest -> go (step state c) rest
  \end{code}
  
  Briefly, the machine begins in some `start` state, then updates its state
  according to the current state and the next input `Char`, and repeats until the
  entire input has been processed. If it ends in a state designated as an
  accepting state, we say the machine accepts the input.
  
  For example, the following DFA accepts strings consisting of an odd number
  of 'x's:
  
  \begin{code}
  oddXs :: Dfa
  oddXs = (0, step, \state -> state == 1) where
    step 0 'x' = 1
    step 1 'x' = 0
    step _  _  = 2
  
  -- This should return True.
  demoOddXs :: Bool
  demoOddXs = runDfa oddXs "xxxxx"
  \end{code}
  
  How many states should we allow? We could say there is one state for every
  possible configuration of the computer save the input, but then we'd simply be
  pushing a problem elsewhere. How can we reason about an automaton with so
  many states? Thus the number of states should be relatively small.
  
  We quickly find
  https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages[DFAs are
  incapable of elementary tasks] such as checking if a bunch of parentheses are
  balanced, or if some number of As is followed by an equal number of Bs.
  
  By the way, we can extend the above to spit out characters as it computes. See
  https://en.wikipedia.org/wiki/Moore_machine[Moore machines] and
  https://en.wikipedia.org/wiki/Mealy_machine[Mealy machines].
  
  == Deterministic Push-Down Automata ==
  
  DFAs are hobbled by lack of memory. Let's fix this. Perhaps the simplest kind
  of memory is a stack, as evidenced by the popularity of stack-based virtual
  machines. We model such machines with _deterministic push-down automata_:
  
  \begin{code}
  type Diff = (State, [Char])
  data DpdaOp = Reject | BlindPush Diff | Push (Char -> Diff)
  type Dpda = (State, Char, State -> Char -> DpdaOp, State -> Bool)
  
  runDpda :: Dpda -> [Char] -> Bool
  runDpda (start, stackInit, step, accepts) s = go start [stackInit] s where
    go state stack s = case stack of
      [] -> False
      top:rest -> case step state top of
        Reject -> False
        BlindPush next -> apply next s
        Push f -> case s of
          "" -> accepts state
          c:cs -> apply (f c) cs
        where apply (nextState, stackDiff) = go nextState (stackDiff ++ rest)
  \end{code}
  
  Informally, the machine starts in a given state with a given symbol on the
  stack. On each step, it examines the stack. If empty, then the machine
  rejects, otherwise it pops off the top of the stack. The current state and the
  popped-off symbol determine the action for this step, which is one of:
  
   * `Reject`: halt the machine and reject the input.
  
   * `BlindPush`: ignore the input, enter a given state and push a given
  sequence of symbols on the stack.
  
   * `Push`: if at the end of input, then halt, accepting if in a given set of
  states. Otherwise consume one character of the input, which may be used to
  determine the next state and the symbols to push.
  
  For example, the following DPDA accepts strings consisting of balanced
  parentheses. As it processes characters from the input string, it records the
  current nesting depth in unary on the stack.
  
  \begin{code}
  balanced :: Dpda
  balanced = (0, '-', step, \state -> state == 0) where
    step 0 '-' = Push (\c -> case c of
      '(' -> (1, "1-")
      _   -> (2, "")
      )
    step 1 '-' = BlindPush (0, "-")
    step 1 '1' = Push (\c -> case c of
      '(' -> (1, "11")
      ')' -> (1, "")
      _   -> (2, "")
      )
    step _ _   = Reject
  
  -- This should return True.
  demoBalanced :: Bool
  demoBalanced = runDpda balanced "(()())"
  \end{code}
  
  It turns out DPDAs are incapable of basic tasks such as checking if the input
  is a palindrome, or if some number of As is followed by an equal number of Bs
  followed by an equal number of Cs.
  
  == Turing Machines ==
  
  DPDAs flounder because the values popped off the stack are lost. What if we
  could save them, say, on a second stack?
  
  Also, the design of DPDAs smells. We have `Char` values on a stack, and another
  bunch of `Char` values in our input string. The former tells us whether to
  bother reading from the latter. There are two edge cases to worry about: the
  empty stack, and the end of input. More than one condition causes the machine
  to halt. Can we simplify?
  
  Let's try starting with two stacks that initially hold the input. We add
  a current state and a current `Char` value that determine our next move,
  which is either to halt, or to do all of the following:
  
    * push a `Char` to one of the stacks;
    * pop off a `Char` from the other, which becomes our next current value; and
    * enter the next state.
  
  This seems promising, but we have limited memory because each push corresponds
  to a pop. We could permit pushing several values at once, but this makes our
  machine uglier.
  
  Better to allow "bottomless" stacks. Rather than rejecting, we
  define the result of popping an empty stack to be a special `Char`
  value that we call a _blank_.
  
  We have just described _Turing machines_.
  Usually, the two stacks and current value are explained in terms of a movable
  read/write head on a tape that is infinitely long in either direction, which is
  disconcerting since it's impossible to cram an infinite tape into a real
  computer, or for that matter, into our universe. Nonetheless we adopt
  mainstream nomenclature in our code. For example, we call a stack a one-way
  tape.
  
  \begin{code}
  data OneWayTape = Char :> OneWayTape
  type Tape = (OneWayTape, Char, OneWayTape)
  data Direction = L | R
  data TMOp = Halt | Step (State, (Char, Direction))
  type TM = (State, State -> Char -> TMOp)
  
  runTM :: TM -> Tape -> Tape
  runTM (start, step) tape = go start tape where
    go state (l, c, r) = case step state c of
      Halt -> (l, c, r)
      Step (nextState, (c', dir)) -> go state (case dir of
        L -> case l of x :> xs -> (xs     , x, c' :> r)
        R -> case r of x :> xs -> (c' :> l, x, xs     )
        )
  \end{code}
  
  We represent a blank with the space character. We encode the input string
  by pushing its characters on one of the stacks, or in conventional terms,
  we write the string immediately to the right of tape head. We expect the
  output to be in the same format.
  
  \begin{code}
  blanks :: OneWayTape
  blanks = ' ' :> blanks
  
  toTape :: [Char] -> Tape
  toTape s      = (blanks, ' ', go s) where
    go ""       = blanks
    go (c:rest) = c :> go rest
  
  fromTape :: Tape -> [Char]
  fromTape (_, _, xs) = go xs where
    go (x :> xt) = if x == ' ' then "" else x:go xt
  
  evalTM :: TM -> String -> String
  evalTM p s = fromTape (runTM p (toTape s))
  \end{code}
  
  We ditch the notion of accepting states; we could trivially support them by
  tweaking any given TM to write a symbol representing acceptance before halting.
  
  https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis[Turing machines
  are a decent mathematical answer to "What is a computer?"]
  Thus we revise our definition of an interpreter, which in turn defines a
  programming language:
  
  ------------------------------------------------------------------------
  interpret :: Language -> TM
  ------------------------------------------------------------------------
  
  == What is a compiler? ==
  
  Let's put all the pieces together. A language is defined by a function
  that maps a given program to a Turing machine. Given two language
  specifications:
  
  ------------------------------------------------------------------------
  interpret :: Language -> TM
  interpretTarget :: TargetLanguage -> TM
  ------------------------------------------------------------------------
  
  a compiler from the first language to the second is a function:
  
  ------------------------------------------------------------------------
  compile :: Language -> TargetLanguage
  ------------------------------------------------------------------------
  
  such that for all source programs `p` and for all strings `s`:
  
  ------------------------------------------------------------------------
  evalTM (interpret p) s == evalTM (interpretTarget (compile p)) s
  ------------------------------------------------------------------------
  
  == What else is there? ==
  
  Researchers have long used interpreters to define programming languages.
  https://aiplaybook.a16z.com/reference-material/mccarthy-1960.pdf[McCarthy's paper on LISP] and
  https://fi.ort.edu.uy/innovaportal/file/20124/1/22-landin_correspondence-between-algol-60-and-churchs-lambda-notation.pdf[Landin's paper on ALGOL 60]
  are classics.
  This technique grew more mathematical over time, evolving into
  https://en.wikipedia.org/wiki/Semantics_(computer_science)[formal semantics].
  Knuth vividly recounts the history in
  https://www.win.tue.nl/~mvdbrand/courses/seminar/0809/papers/ag-genesis.pdf[a
  paper on attribute grammars]. (Attribute grammars are a venerable branch of
  formal semantics; see Backhouse,
  https://link.springer.com/content/pdf/10.1007/3-540-46002-0_11.pdf[_A
  Functional Semantics of Attribute Grammars_] for a modern take.)
  
  https://smlfamily.github.io/sml97-defn.pdf[Standard ML] is the gold standard.
  
  https://webassembly.github.io/spec/core/exec/index.html[WebAssembly] was also designed hand-in-hand with its formal semantics.
  
  Incredibly, formal semantics exist for a substantial subset of C.
  Attempting to formalize all of C is a fool's errand. For example:
  
    * Officially, https://blog.regehr.org/archives/232[it is illegal to optimize
    `x=0; x=0;`] but this rule is flouted in practice.
    * https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201901-popl-cerberus.pdf[Pointer
    semantics are ill-defined]. https://gcc.godbolt.org/z/6dvd7c[Try for yourself online]!
    We sympathize with: "...the ISO standard is a prose document, as is typical
    for industry standards. The lack of mathematical precision, while also
    typical for industry standards, has surely contributed to the accumulated
    confusion..."
    * https://queue.acm.org/detail.cfm?id=3468263[Meaningless C/C++ is often
    found in production. The `memmove()` function is difficult to write in C].
  
  There is even http://compcert.inria.fr/[a certified C compiler], that is, a C
  compiler that a computer can prove is correct.
  
  Cryptographers eventually joined the fun in 1982, when Goldwasser and Micali
  defined https://en.wikipedia.org/wiki/Semantic_security[semantic security].
  Canetti later defined
  https://en.wikipedia.org/wiki/Universal_composability[universal composability].
  
  https://www.youtube.com/watch?v=bmKYiUOEo2A[Conal Elliot gave an inspiring talk
  on _denotational design_]. He advocates mathematical thinking beyond its
  traditional strongholds, and in particular shows how it applies to manipulating
  images. See also
  https://www.youtube.com/watch?v=j3Q32brCUAI[Functional Reactive Programming]
  and
  https://www.youtube.com/watch?v=teRC_Lf61Gw[Functional Reactive Programming,
  more elegantly specified].
  
  Even
  https://www.microsoft.com/en-us/research/uploads/prod/2018/03/build-systems-final.pdf[build
  systems] and operating systems
  (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf[seL4],
  http://flint.cs.yale.edu/certikos/[CertiKOS]) can be defined mathematically.
  
  https://en.wikipedia.org/wiki/Montague_grammar[Richard Montague] believed that
  with enough research, we can show natural languages are no different to formal
  languages, so perhaps there exists a non-mathematical path to precision.
  
  Decades ago,
  http://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf[some argued against
  getting too formal with programming languages]. Later,
  https://eprint.iacr.org/2004/152.pdf[some cryptographers argued similarly
  against provable security]
  (https://eprint.iacr.org/2019/1336.pdf[see also its sequel]).
  This stance seems incompatible with Montague's.
  