Tidied up the HATRA paper again

papers/hatra21/bibliography.bib

@@ -34,3 +34,19 @@
   url =          {https://corp.roblox.com/2020/07/roblox-developers-expected-earn-250-million-2020-platform-now-150-million-monthly-active-users/},
 }
 
+@Book{TAPL,
+  author =       {Benjamin C. Pierce},
+  title =        {Types and Programming Languages},
+  publisher =    {{MIT} Press},
+  year =         {2002},
+  isbn =         {0-262-16209-1},
+}
+
+@Book{TDDIdris,
+  author =       {Edwin Brady},
+  title =        {Type-Driven Development with {Idris}},
+  publisher =    {Manning},
+  year =         {2017},
+  isbn =         {9781617293023},
+}
+

papers/hatra21/hatra21.tex

@@ -95,11 +95,36 @@ documentation).
 
 \subsection{Type-driven development}
 
-- Code refactoring
+Professional development studios are also goal-directed (though the
+goals may be more abstract, such as ``decrease user churn'' or
+``improve frame rate'') but have needs that are less common in
+learners:
+\begin{itemize}
 
-- Code navigation
+\item \emph{Code planning}:
+  code spends much of its development time in an incomplete state,
+  with holes that will be filled in later.
 
-- Detect detection
+\item \emph{Code refactoring}:
+  experiences evolve over time, and it easy for changes to
+  break previously-held invariants.
+
+\item \emph{Defect detection}:
+  code has errors, and detecting these at runtime (for example by crash telemetry)
+  can be expensive and recovery can be time-consuming.
+  
+\end{itemize}
+Detecting defects ahead-of-time is a traditional goal of type systems,
+resulting in an array of techniques for establishing safety results,
+surveyed for example in~\cite{TAPL}. Supporting code planning and
+refactoring are some of the goals of \emph{type-driven
+development}~\cite{TDDIdris} under the slogan ``type, define,
+refine''.
+
+To help support the transition from novice to experienced developer,
+types are introduced gradully, through API documentation and type discovery.
+Type inference provides many of the benefits of type-driven development
+even to creators who are not explicitly providing types.
 
 \section{Types}
 \subsection{Infallible types}