Index: doc/theses/mike_brooks_MMath/intro.tex
===================================================================
--- doc/theses/mike_brooks_MMath/intro.tex	(revision 41fb996a500250f2d0a7d1f16e6147ada3c96f01)
+++ doc/theses/mike_brooks_MMath/intro.tex	(revision 486caad7c0e53d562d8675ebf6836c087eaa427b)
@@ -1,6 +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.
+All modern programming languages provide three high-level containers (collection): array, linked-list, and string.
+Often array is part of the programming language, while linked-list is built from pointer types, and string from a combination of array and linked-list.
 
 \cite{Blache19}
@@ -17,8 +17,8 @@
 \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;
+Linked-list provides a homogeneous container with $O(log N)$/$O(N)$ access to elements using successor and predecessor operations.
+Subscripting by value is sometimes available, \eg hash table.
+Linked types are normally dynamically sized by adding/removing nodes using link fields internal or external to the elements (nodes).
+If a programming language allows pointer to stack storage, linked-list types can be allocated on the stack;
 otherwise, elements are heap allocated and explicitly/implicitly managed.
 
@@ -35,6 +35,6 @@
 \section{Motivation}
 
-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 C.
-Unfortunately, to make C better while retaining a high level of backwards compatibility requires a significant knowledge of C's design.
+The goal of this work is to introduce safe and complex versions of array, link-lists, and string into the programming language \CFA~\cite{CFA}, which is based on C.
+Unfortunately, to make C better, while retaining a high level of backwards compatibility, requires a significant knowledge of C's design.
 Hence, it is assumed the reader has a medium knowledge of C or \CC, on which extensive new C knowledge is built.
 
@@ -42,13 +42,13 @@
 \subsection{C?}
 
-Like many established programming languages, C has a standards committee and multiple ANSI/ISO language manuals~\cite{C99,C11,C18,C23}.
-However, most programming languages are only partially explained by these manuals.
+Like many established programming languages, C has a standards committee and multiple ANSI/\-ISO language manuals~\cite{C99,C11,C18,C23}.
+However, most programming languages are only partially explained by standard's manuals.
 When it comes to explaining how C works, the definitive source is the @gcc@ compiler, which is mimicked by other C compilers, such as Clang~\cite{clang}.
-Often other C compilers must \emph{ape} @gcc@ because a large part of the C library (runtime) system is embedded with @gcc@ features.
+Often other C compilers must \emph{ape} @gcc@ because a large part of the C library (runtime) system contains @gcc@ features.
 While some key aspects of C need to be explained by quoting from the language reference manual, to illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and shows its behaviour.
 These example programs show
 \begin{itemize}
 	\item the compiler accepts or rejects certain syntax,
-	\item the prints output to buttress a claim of behaviour,
+	\item prints output to buttress a claim of behaviour,
 	\item executes without triggering any embedded assertions testing pre/post-assertions or invariants.
 \end{itemize}
@@ -77,5 +77,5 @@
 with a segmentation fault at runtime.
 Clearly, @gcc@ understands these ill-typed case, and yet allows the program to compile, which seems like madness.
-Compiling with @-Werror@, which turns warnings into errors, is often too strong, because some warnings are just warnings.
+Compiling with flag @-Werror@, which turns warnings into errors, is often too strong, because some warnings are just warnings.
 In the following discussion, ``ill-typed'' means giving a nonzero @gcc@ exit condition with a message that discusses typing.
 Note, \CFA's type-system rejects all these ill-typed cases as type mismatch errors.