Index: doc/theses/mike_brooks_MMath/intro.tex
===================================================================
--- doc/theses/mike_brooks_MMath/intro.tex	(revision f5212cad726a1a738cd752a14c20f57c84087c14)
+++ doc/theses/mike_brooks_MMath/intro.tex	(revision bdc859191d5e3bb951a9d9d51d18b341a48ab190)
@@ -1,3 +1,6 @@
 \chapter{Introduction}
+
+All modern programming languages provide three high-level containers (collection): array, linked, and string.
+Often array is part of the programming language, while linked is built from pointer types, and string from a combination of array and linked.
 
 \cite{Blache19}
@@ -5,7 +8,102 @@
 \cite{Ruef19}
 
-\section{Arrays}
+\section{Array}
 
-\section{Strings}
+Array provides a homogeneous container with $O(1)$ access to elements using subscripting.
+The array size can be static, dynamic but fixed after creation, or dynamic and variable after creation.
+For static and dynamic-fixed, an array can be stack allocated, while dynamic-variable requires the heap.
+
+
+\section{Linked List}
+
+Linked provides a homogeneous container with $O(log N)$/$O(N)$ access to elements using successor and predecessor operations.
+Subscripting by value is sometimes available.
+Linked types are normally dynamically sized by adding/removing node using link fields internal or external to the elements (nodes).
+If a programming language allows pointer to stack storage, linked types can be allocated on the stack;
+otherwise, elements are heap allocated and explicitly/implicitly managed.
+
+
+\section{String}
+
+String provides a dynamic array of homogeneous elements, where the elements are often human-readable characters.
+What differentiates string from other types in that string operations work on blocks of elements for scanning and changing the elements, rather than accessing individual elements.
+Nevertheless, subscripting is often available.
+The cost of string operations is less important than the power of the block operation to accomplish complex manipulation.
+The dynamic nature of string means storage is normally heap allocated but often implicitly managed, even in unmanaged languages.
+
+
+\section{C/\CFA}
+
+The goal of this work is to introduce safe and complex versions of array, link, and string into the programming language \CFA, which based on the C.
+
+
+\subsection{Common knowledge}
+
+The reader is assumed to have used C or \CC for the coursework of at least four university-level courses, or have equivalent experience.
+The current discussion introduces facts, unaware of which, such a functioning novice may be operating.
+
+% TODO: decide if I'm also claiming this collection of facts, and test-oriented presentation is a contribution; if so, deal with (not) arguing for its originality
+
+\subsection{Convention: C is more touchable than its standard}
+
+When it comes to explaining how C works, I like illustrating definite program semantics.
+I prefer doing so, over a quoting manual's suggested programmer's intuition, or showing how some compiler writers chose to model their problem.
+To illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and I show its behaviour.
+
+This behaviour is typically one of
+\begin{itemize}
+	\item my statement that the compiler accepts or rejects the program
+	\item the program's printed output, which I show
+	\item my implied assurance that its assertions do not fail when run
+\end{itemize}
+
+The compiler whose program semantics is shown is
+\begin{cfa}
+$ gcc --version
+gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0
+\end{cfa}
+running on Architecture @x86_64@, with the same environment targeted.
+
+Unless explicit discussion ensues about differences among compilers or with (versions of) the standard, it is further implied that there exists a second version of GCC and some version of Clang, running on and for the same platform, that give substantially similar behaviour.
+In this case, I do not argue that my sample of major Linux compilers is doing the right thing with respect to the C standard.
+
+
+\subsection{C reports many ill-typed expressions as warnings}
+
+These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
+\lstinput{12-15}{bkgd-c-tyerr.c}
+with warnings:
+\begin{cfa}
+warning: assignment to 'float *' from incompatible pointer type 'void (*)(void)'
+warning: assignment to 'void (*)(void)' from incompatible pointer type 'float *'
+\end{cfa}
+Similarly,
+\lstinput{17-19}{bkgd-c-tyerr.c}
+with warning:
+\begin{cfa}
+warning: passing argument 1 of 'f' from incompatible pointer type
+note: expected 'void (*)(void)' but argument is of type 'float *'
+\end{cfa}
+with a segmentation fault at runtime.
+
+That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@.
+Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition.
+
+A "tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute"*1 rejected the program.
+The behaviour (whose absence is unprovable) is neither minor nor unlikely.
+The rejection shows that the program is ill-typed.
+
+Yet, the rejection presents as a GCC warning.
+
+In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing.
+
+*1  TAPL-pg1 definition of a type system
+
 
 \section{Contributions}
+
+\subsection{Linked List}
+
+\subsection{Array}
+
+\subsection{String}