Index: doc/theses/mike_brooks_MMath/intro.tex
===================================================================
--- doc/theses/mike_brooks_MMath/intro.tex	(revision 43b65162ba86dd37539662ef821c6bcdc049f924)
+++ doc/theses/mike_brooks_MMath/intro.tex	(revision c979afa73690329eb48a020518c303ebd051663a)
@@ -11,22 +11,29 @@
 In a study of software exploits in the U.S. National Vulnerability Database over 2013--2017, the top reported vulnerability is buffer errors (in the sense of misused array bounds), among 19 vulnerability categories~\cite{Cifuentes19}.
 
-While these figures address memory errors, defined without limit to the three primary collections, these authors' explanations of memory errors, among other C analysis efforts, suggest improving on C's language/library options for working with these three collections would be widely beneficial.
+While these figures address memory errors, not limited to the three primary collections, the authors' explanations of memory errors suggest improving on C's language/library options for working with the three collections would be beneficial.
 Every one of the safety-statistic sources above includes array bounds in its first characterization of unsafe programming-language features.
 Of the four studies that deal exclusively with memory safety (excluding~\cite{Cifuentes19}), all put @malloc@--@free@ upfront as well.
-The one that specifically surveys C features, \cite{Oorschot23}, also has similarly prominent blame on both of: the null-terminated text idiom, with its support/mandate in the C standard library; the unprotected nature of C pointers.
-An effort at translating C to safe Rust~\cite{Emre2022} has pointers as the stand-out difficult aspect to analyze.\footnote{
-	\cite{Emre2022} demonstrates the difficulty of analyzing C pointers for safety (while tacking some of this difficult problem).
-	It first puts a corpus of C programs through a naive Rust translation, which ``succeeds'' by leaving many uses of Rust's \lstinline{unsafe} marker.
-	Then, it analyzes these uses and presents a technique for reducing those uses that hinge exclusively on referenced object lifetime.
-	Pointer dereference accounts for 80\% of the cases that the naive translation did not make safe (Table 3.2, p33).
-	Of these, 10\% are eligible for the work's own safety improvement technique, while this filtering leaves 75\% with no single cause of unsafety determined (Table 3.5, p39).
-	The presented technique succeeds at making 75\% of the eligible initially unsafe dereferences safe, by inferring the necessary lifetime annotations (Table 4.2, p83).
-	This result leaves, per 1000 LOC, 3.3 unremovable unsafe dereferences that are understood to evade lifetime analysis, among 220 gross unsafe dereferences (Tables 3.5, 4.2 and 3.1, p27).
-	% 3.3 = 1398/413,428 * 1000
-	% 220 ~= (99,101 [@tab3.5] - 9631 [@tab4.2] ) / 413,428 [@tab 3.1] * 1000
-}
+The specific survey of C features, \cite{Oorschot23}, also places blame on:
+\begin{itemize}
+\item
+the null-terminated text idiom, with its support/mandate in the C standard library and
+\item
+the unprotected nature of C pointers.
+\end{itemize}
+
+An effort at translating C to safe Rust~\cite{Emre2022} has pointers as the stand-out difficult aspect to analyze.
+It demonstrates the difficulty of analyzing C pointers for safety.
+It first puts a corpus of C programs through a naive Rust translation, which ``succeeds'' by leaving many uses of Rust's \lstinline{unsafe} marker.
+Then, it analyzes these uses and presents a technique for reducing the uses that hinge exclusively on referenced object lifetime.
+Pointer dereference accounts for 80\% of the cases that the na\"{i}ve translation did not make safe (Table 3.2, p.~33).
+Of these, 10\% are eligible for the work's own safety improvement technique, while this filtering leaves 75\% with no single cause of unsafety determined (Table 3.5, p.~39).
+The presented technique succeeds at making 75\% of the eligible initially unsafe dereferences safe, by inferring the necessary lifetime annotations (Table 4.2, p.~83).
+This result leaves, per 1000 LOC, 3.3 unremovable unsafe dereferences that are understood to evade lifetime analysis, among 220 gross unsafe dereferences (Tables 3.5, 4.2 and 3.1, p.~27).
+% 3.3 = 1398/413,428 * 1000
+% 220 ~= (99,101 [@tab3.5] - 9631 [@tab4.2] ) / 413,428 [@tab 3.1] * 1000
+
 A tool for analyzing C code's use of linked data structures (including, \eg skip list and binary tree) found variations of the linked-list shape to be present in most of the programs in its corpus~\cite{White2016}.
-So, C's array unsafety is infamous, its string pattern necessitates explicit storage management (also infamous), and user-written linked lists are an attrictively recognizable player in the arena of (infamously) unsafe raw pointer uses.
-Therefore, hardening the three primary collections goes a long way to making the majority of C programs safer, and eliminating major hacker attack vectors.
+So, C's array unsafety is infamous, its string pattern necessitates explicit storage management (also infamous), and user-written linked lists are a recognizable player in the arena of (infamously) unsafe raw pointer uses.
+Therefore, hardening the three primary collections goes a long way to making the majority of C programs safer, eliminating major hacker attack vectors.
 
 This work looks at extending these foundational container types in the programming language \CFA, which is a new dialect of the C programming language.
@@ -46,8 +53,9 @@
 For static and dynamic-fixed, an array can be stack allocated, while dynamic-variable requires the heap.
 Because array layout has contiguous components, subscripting is a computation, \ie some form of pointer arithmetic.
+Not included in this requirement are pseudo-arrays with arbitrary keys, \eg hash table subscripted by a string key (see below).
 
 C provides a simple array type as a language feature.
 However, it adopts the controversial position of treating pointer and array as twins, leading to multiple problems.
-The way that arrays are typicaly passed around a program removes the information necessary to do bound checks.
+Hence, the way that arrays are typically passed around in a program removes the information necessary to do bound checks.
 
 
@@ -77,11 +85,11 @@
 Therefore, the cost of a string operation is usually less important than the power of the operation to accomplish complex text manipulation, \eg search, analysing, composing, and decomposing string text.
 The dynamic nature of a string means storage is normally heap allocated but often implicitly managed, even in unmanaged languages.
-In many cases, string management is separate from heap management, \ie strings roll their own heap.
+In many cases, string management is separate from heap management, \ie strings roll-their-own heap.
 
 The C string type is just a character array and requires user storage-management to handle varying size.
 C adopts a terminating sentinel character, @'\0'@, to mark the end of a variable-length character-array versus a preceding length field.
-Hence, the sentinel character is excluded from a string and determining the string length is an $O(N)$ operation.
+Hence, the sentinel character is excluded as an element within a string and determining the string length is an $O(N)$ operation.
 The C standard library includes a number of high-level operations for working with this representation.
-Most of these operations are awkward to use and error prone.
+Most of these operations are awkward to use and highly error prone.
 
 
@@ -103,7 +111,7 @@
 The three primary container types in C are difficult to understand, teach, and get right because they are too low level.
 Providing higher-level, feature-rich versions of these containers in \CFA is a major component of the primary goal.
-The result is a simplify programming experience, which increases productivity and maintainability.
-\item
-The new container types must be as correct and safe to use as those in other modern programming languages, which has been shown to a primary concern of industry, government, and military~\cite{ONCD}.
+The result is a simplified programming experience, which increases productivity and maintainability.
+\item
+The new container types must be as correct and safe to use as those in other modern programming languages, to elide the concerns of industry, government, and military~\cite{ONCD}.
 Prior approaches focus on out-of-bound array accesses using a model-based approach (ASCET) in embedded systems (\eg cars)~\cite{Blache19}, and general and null-terminated string arrays using a \CC template syntax (Checked C)~\cite{Elliott18,Ruef19}.
 Both White House~\cite{WhiteHouse24} and DARPA~\cite{DARPA24} recently released a recommendation to \emph{move away} from C and \CC, because of cybersecurity threats exploiting vulnerabilities in these languages.
@@ -111,5 +119,5 @@
 \end{enumerate}
 
-While new languages, \eg Go, Rust, Swift, purport to be systems languages replacing C, the reality is that rewriting massive C code-bases is impractical and a non-starter if the runtime uses garbage collection.
+While new languages, \eg Go, Rust, Swift, purport to be systems languages replacing C, the reality is that rewriting massive C code-bases is impractical and a non-starter if the runtime uses garbage collection~\cite{Brinker26}.
 Even assuming automated conversion of C programs to other safe languages, who will maintain this massive new code-base?
 Furthermore, new languages must still interact with the underlying C operating system through fragile, type-unsafe, interlanguage-communication.
@@ -142,5 +150,5 @@
 Overall, this work has produced significant syntactic and semantic improvements to C's arrays, linked-lists and string types.
 % As well, a strong plan for general iteration has been sketched out.
-The following are the detailed contributions, where performance and safety were always the motivating factors.
+The following are the detailed contributions, where performance and safety are always the motivating factors.
 
 \subsection{Array}
@@ -172,5 +180,5 @@
 \subsection{String}
 
-The new string type and its runtime library are available through @#include <string.hfa>@.
+A new string type and its runtime library are available through @#include <string.hfa>@.
 The library offers a type where basic usage is comparable to the \CC @string@ type, including analogous coexistence with raw-character pointers.
 Its implementation, however, follows different principles, enabling programs to work with strings by value, without incurring excessive copying.
Index: doc/theses/mike_brooks_MMath/uw-ethesis.bib
===================================================================
--- doc/theses/mike_brooks_MMath/uw-ethesis.bib	(revision 43b65162ba86dd37539662ef821c6bcdc049f924)
+++ doc/theses/mike_brooks_MMath/uw-ethesis.bib	(revision c979afa73690329eb48a020518c303ebd051663a)
@@ -1,3 +1,3 @@
-% Bibliography of key references for "LaTeX for Thesis and Large Documents"
+f% Bibliography of key references for "LaTeX for Thesis and Large Documents"
 % For use with BibTeX
 
@@ -126,25 +126,25 @@
 
 @phdthesis{Emre2022,
-    author  = "Mehmet Emre",
-    title   = "Translating C to Safe Rust: Reasoning about Pointer Types and Lifetimes",
-    school  = "UC Santa Barbara",
-    year    = "2022"
+    author	= "Mehmet Emre",
+    title	= "Translating C to Safe Rust: Reasoning about Pointer Types and Lifetimes",
+    school	= "UC Santa Barbara",
+    year	= 2022
 }
 
 @inproceedings{White2016,
-    author = {White, David H. and Rupprecht, Thomas and L\"{u}ttgen, Gerald},
-    title = {DSI: an evidence-based approach to identify dynamic data structures in C programs},
-    year = {2016},
-    isbn = {9781450343909},
-    publisher = {Association for Computing Machinery},
-    address = {New York, NY, USA},
-    url = {https://doi.org/10.1145/2931037.2931071},
-    doi = {10.1145/2931037.2931071},
-    booktitle = {Proceedings of the 25th International Symposium on Software Testing and Analysis},
-    pages = {259–269},
-    numpages = {11},
-    keywords = {Data structure identification, dynamic data structures, pointer programs, program comprehension},
-    location = {Saarbr\"{u}cken, Germany},
-    series = {ISSTA 2016}
+    author	= {White, David H. and Rupprecht, Thomas and L\"{u}ttgen, Gerald},
+    title	= {DSI: an evidence-based approach to identify dynamic data structures in C programs},
+    year	= {2016},
+    isbn	= {9781450343909},
+    publisher	= {Association for Computing Machinery},
+    address	= {New York, NY, USA},
+    url	= {https://doi.org/10.1145/2931037.2931071},
+    doi	= {10.1145/2931037.2931071},
+    booktitle	= {Proceedings of the 25th International Symposium on Software Testing and Analysis},
+    pages	= {259-269},
+    numpages	= {11},
+    keywords	= {Data structure identification, dynamic data structures, pointer programs, program comprehension},
+    location	= {Saarbr\"{u}cken, Germany},
+    series	= {ISSTA 2016}
 }
 
@@ -180,2 +180,14 @@
 }
 
+@article{Brinker26,
+    author	= {Brinker, Andrew Lilley},
+    title	= {Memory Safety for Skeptics},
+    year	= {2026},
+    publisher	= {ACM},
+    address	= {New York, NY, USA},
+    volume	= {69},
+    number	= {2},
+    journal	= {CACM},
+    month	= jan,
+    pages	= {52-58},
+}