WIP: Edit Preface

default.nix

@@ -51,6 +51,8 @@ with import nixpkgs {
       xelatex = super.texlive.combine {
         inherit (super.texlive) scheme-small
           amsmath
+          biber
+          biblatex
           datatool
           dirtytalk
           ebproof
@@ -61,11 +63,14 @@ with import nixpkgs {
           ifplatform
           latexmk
           lm-math
+          logreq
           mfirstuc
           minted
           newunicodechar
+          outlines
           substr
           todonotes
+          tracklang
           xetex
           xfor
           xindy

src/book.bib

@@ -0,0 +1,32 @@
+@online{plf,
+  title   = {Programming Language Foundations},
+  author  = {Pierce, Benjamin C. and de Amorim, Arthur Azevedo and Casinghino,
+             Chris and Gaboardi, Marco and Greenberg, Michael and Hriţcu,
+             Cătălin and Sjöberg, Vilhelm and Tolmach, Andrew and Yorgey,
+             Brent},
+  date    = {2018},
+  month   = {aug},
+  url     = {https://softwarefoundations.cis.upenn.edu/plf-current/index.html},
+  urldate = {2018-11-02}
+}
+
+@online{sf,
+  title   = {Software Foundations},
+  author  = {Pierce, Benjamin C. and de Amorim, Arthur Azevedo and Casinghino,
+             Chris and Gaboardi, Marco and Greenberg, Michael and Hriţcu,
+             Cătălin and Sjöberg, Vilhelm and Tolmach, Andrew and Yorgey,
+             Brent and Appel, Andrew W. and Lampropoulos, Leonidas},
+  date    = {2018},
+  month   = {aug},
+  url     = {https://softwarefoundations.cis.upenn.edu},
+  urldate = {2018-11-02}
+}
+
+@online{vfa,
+  title   = {Verified Functional Algorithms},
+  author  = {Appel, Andrew W.},
+  date    = {2018},
+  month   = {aug},
+  url     = {https://softwarefoundations.cis.upenn.edu/vfa-current/index.html},
+  urldate = {2018-11-02}
+}

src/book.tex

@@ -23,6 +23,8 @@
 papersize: b5
 geometry: margin=1in
 header-includes:
+- \usepackage[american]{babel}
+-
 - \setmonofont{Iosevka}
 -
 - \usepackage[utf8]{inputenc}
@@ -34,6 +36,7 @@
 - \usemintedstyle{lovelace}
 - \newmintinline[el]{elisp}{}
 - \newmintinline[idr]{idris}{}
+- \newmintinline[txt]{text}{}
 -
 - \usepackage[xindy]{glossaries}
 - \makeglossaries
@@ -44,6 +47,12 @@
 -
 - \usepackage{ebproof}
 - \usepackage{dirtytalk}
+-
+- \usepackage{outlines}
+-
+- \usepackage[backend=biber, dateabbrev=false, hyperref=true, style=numeric]{biblatex}
+- \newcommand{\citefieldlink}[2]{\hyperlink{cite.\therefsection @#1}{\textit{\citefield{#1}{#2}}}}
+- \addbibresource{book.bib}
 include-before: \frontmatter
 ---
 

src/footer.tex

@@ -1 +1,78 @@
+\chapter{Postscript}
+\label{postscript}
+
+Congratulations: We've made it to the end!
+
+\section{Looking Back}
+
+We've covered quite a bit of ground so far. Here's a quick review...
+
+\begin{outline}
+\1 \Gls{functional programming}:
+  \2 ``declarative'' programming style (recursion over immutable data
+  structures, rather than looping over mutable arrays or pointer structures)
+  \2 higher-order functions
+  \2 polymorphism
+\1 \textit{Logic}, the mathematical basis for software engineering:
+  \[
+    \frac{\text{logic}}{\text{software engineering}} \sim
+    \frac{\text{calculus}}{\text{mechanical/civil engineering}}
+  \]
+  \2 inductively defined sets and relations
+  \2 inductive proofs
+  \2 proof objects
+\1 \textit{Idris}, a dependently-typed programming language
+  \2 functional core language
+  \2 full \glspl{dependent type}
+  \2 \gls{dependent pattern matching}
+  \2 powerful \glspl{elaboration reflection}
+\end{outline}
+
+
+\section{Looking Forward}
+
+If what you've seen so far has whetted your interest, you have two choices for
+further reading in the \citefieldlink{sf}{title} series:
+
+\begin{outline}
+\1 \citefieldlink{plf}{title} (volume 2, by a set of authors similar to this
+  book's) covers material that might be found in a graduate course on the theory
+  of programming languages, including Hoare logic, operational semantics, and
+  type systems.
+\1 \citefieldlink{vfa}{title} (volume 3, by Andrew Appel) builds on the themes
+  of functional programming and program verification in Coq, addressing a range
+  of topics that might be found in a standard data structures course, with an
+  eye to formal verification.
+\end{outline}
+
+
+\section{Other sources}
+
+Here are some other good places to learn more...
+
+\begin{outline}
+\1 This book includes some optional chapters covering topics that you may
+  find useful. Take a look at the table of contents and the chapter dependency
+  diagram to find them.
+\1 \todo[inline]{Mention Idris on StackOverflow}
+\todo{Bibliography entries}
+\1 Here are some great books on functional programming
+  \2 Learn You a Haskell for Great Good, by Miran Lipovaca [Lipovaca
+    2011].
+  \2 Real World Haskell, by Bryan O'Sullivan, John Goerzen, and Don
+  Stewart [O'Sullivan 2008]
+  \2 ...and many other excellent books on Haskell, OCaml, Scheme, Racket,
+  Scala, F$^\sharp$, etc., etc.
+  \todo[inline]{And some further resources for Idris}
+\1 If you're interested in real-world applications of formal verification to
+  critical software, see the Postscript chapter of \citefieldlink{plf}{title}.
+\1 For applications of Coq in building verified systems, the lectures and
+  course materials for the 2017 DeepSpec Summer School are a great
+  resource. \url{https://deepspec.org/event/dsss17/index.html}
+\end{outline}
+
+\phantomsection
 \printglossaries
+
+\phantomsection
+\printbibliography

src/glossary.tex

@@ -10,12 +10,37 @@
   description={\todo{define}}
 }
 
+\newglossaryentry{dependent pattern matching}
+{
+  name={dependent pattern matching},
+  description={\todo{define}}
+}
+
+
+\newglossaryentry{dependent type}
+{
+  name={dependent type},
+  description={\todo{define}}
+}
+
+\newglossaryentry{elaboration reflection}
+{
+  name={elaboration reflection},
+  description={\todo{define}}
+}
+
 \newglossaryentry{expression}
 {
   name={expression},
   description={\todo{define}}
 }
 
+\newglossaryentry{extreme programming}
+{
+  name={extreme programming},
+  description={\todo{define}}
+}
+
 \newglossaryentry{first-class}
 {
   name={first-class},
@@ -36,7 +61,7 @@
 
 \newglossaryentry{functional programming}
 {
-  name={function programming},
+  name={functional programming},
   description={\todo{define}}
 }
 
@@ -85,18 +110,36 @@
   prefix argument sets the recursion depth directly.
 }
 
+\newglossaryentry{imperative}
+{
+  name={imperative},
+  description={\todo{define}}
+}
+
 \newglossaryentry{induction}
 {
   name={induction},
   description={\todo{define}}
 }
 
+\newglossaryentry{inductive proof}
+{
+  name={inductive proof},
+  description={\todo{define}}
+}
+
 \newglossaryentry{inductive rule}
 {
   name={inductive rule},
   description={\todo{define}}
 }
 
+\newglossaryentry{logic}
+{
+  name={logic},
+  description={\todo{define}}
+}
+
 \newglossaryentry{module system}
 {
   name={module system},
@@ -115,9 +158,31 @@
   description={\todo{define}}
 }
 
-\newglossaryentry{proof assistant}
+\newglossaryentry{proof}
 {
-  name={proof assistant},
+  name={proof},
+  description={unassailable arguments for the truth of a particular
+  proposition},
+  descriptionplural={unassailable arguments for the truth of particular
+  propositions},
+  firstplural={\glsentryplural{proof} -- \glsentrydescplural{proof}}
+}
+
+\newglossaryentry{pub-sub}
+{
+  name={publish-subscribe},
+  description={\todo{define}}
+}
+
+\newglossaryentry{pure}
+{
+  name={pure},
+  description={\todo{define}}
+}
+
+\newglossaryentry{side effect}
+{
+  name={side effect},
   description={\todo{define}}
 }
 
@@ -152,8 +217,43 @@
   description={\todo{define}}
 }
 
+\newglossaryentry{value}
+{
+  name={value},
+  description={\todo{define}}
+}
+
 \newglossaryentry{wildcard pattern}
 {
   name={wildcard pattern},
   description={\todo{define}}
 }
+
+
+
+
+\newglossaryentry{proof assistant}{
+  name={proof assistant},
+  description={\todo{define}},
+  see=[see also]{proof}
+}
+
+\newglossaryentry{automated theorem prover}
+{
+  name={automated theorem prover},
+  description={\todo{define}},
+  see=[see also]{proof assistant}
+}
+
+
+
+
+\newacronym{aop}{AOP}{aspect-oriented programming}
+
+\newacronym{oop}{OOP}{object-oriented programming}
+
+\newacronym{mvc}{MVC}{model-view-controller}
+
+\newacronym{sat}{SAT}{Boolean (or propositional) satisfiability}
+
+\newacronym{smt}{SMT}{satisfiability modulo theories}