Index: doc/theses/mike_brooks_MMath/array.tex
===================================================================
--- doc/theses/mike_brooks_MMath/array.tex	(revision 1e110bffa193f11fc02b3e412b060f1b5bcfea22)
+++ doc/theses/mike_brooks_MMath/array.tex	(revision 5a553e2df9bdb97f72584d0230a506cd8c69456a)
@@ -2,62 +2,64 @@
 \label{c:Array}
 
+
 \section{Introduction}
 
-This chapter describes my contribution of language and library features that provide a length-checked array type, as in:
-
-\begin{lstlisting}
-array(float, 99) x;    // x contains 99 floats
-
-void f( array(float, 42) & a ) {}
-f(x);                  // statically rejected: types are different
+Arrays in C are possible the single most misunderstood and incorrectly used features in the language, resulting in the largest proportion of runtime errors and security violations.
+This chapter describes the new \CFA language and library features that introduce a length-checked array-type to the \CFA standard library~\cite{Cforall}, \eg:
+\begin{cfa}
+@array( float, 99 )@ x;					$\C{// x contains 99 floats}$
+void f( @array( float, 42 )@ & p ) {}	$\C{// p accepts 42 floats}$
+f( x );									$\C{// statically rejected: types are different, 99 != 42}$
 
 forall( T, [N] )
-void g( array(T, N) & a, int i ) {
-	T elem = a[i];     // dynamically checked: requires 0 <= i < N
-}
-g(x, 0);               // T is float, N is 99, succeeds
-g(x, 1000);            // T is float, N is 99, dynamic check fails
-\end{lstlisting}
-
-This example first declares @x@ a variable, whose type is an instantiation of the generic type named @array@, with arguments @float@ and @99@.
-Next, it declares @f@ as a function that expects a length-42 array; the type system rejects the call's attempt to pass @x@ to @f@, because the lengths do not match.
-Next, the @forall@ annotation on function @g@ introduces @T@ as a familiar type parameter and @N@ as a \emph{dimension} parameter, a new feature that represents a count of elements, as managed by the type system.
-Because @g@ accepts any length of array; the type system accepts the calls' passing @x@ to @g@, inferring that this length is 99.
-Just as the caller's code does not need to explain that @T@ is @float@, the safe capture and communication of the value @99@ occurs without programmer involvement.
-In the case of the second call (which passes the value 1000 for @i@), within the body of @g@, the attempt to subscript @a@ by @i@ fails with a runtime error, since $@i@ \nless @N@$.
-
-The type @array@, as seen above, comes from my additions to the \CFA standard library.
-It is very similar to the built-in array type, which \CFA inherits from C.
+void g( @array( T, N )@ & p, int i ) {
+	T elem = p[i];						$\C{// dynamically checked: requires 0 <= i < N}$
+}
+g( x, 0 );								$\C{// T is float, N is 99, dynamic subscript check succeeds}$
+g( x, 1000 );							$\C{// T is float, N is 99, dynamic subscript check fails}$
+\end{cfa}
+This example declares variable @x@, with generic type @array@ using arguments @float@ and @99@.
+Function @f@ is declared with an @array@ parameter of length @42@.
+The call @f( x )@ is invalid because the @array@ lengths @99@ and @42@ do not match.
+Next, function @g@ introduces a @forall@ prefix on type parameter @T@ and arbitrary \emph{dimension parameter} @N@, the new feature that represents a count of elements managed by the type system.
+The call @g( x, 0 )@ is valid because @g@ accepts any length of array, where the type system infers @float@ for @T@ and length @99@ for @N@.
+Inferring values for @T@ and @N@ is implicit without programmer involvement.
+Furthermore, the runtime subscript @x[0]@ (parameter @i@ is @0@) in @g@ is valid because @0@ is in the dimension range $[0,99)$ of argument @x@.
+The call @g( x, 1000 )@ is also valid;
+however, the runtime subscript @x[1000]@ is invalid (generates a subscript error) because @1000@ is outside the dimension range $[0,99)$ of argument @x@.
+
+The generic @array@ type is similar to the C array type, which \CFA inherits from C.
 Its runtime characteristics are often identical, and some features are available in both.
-
-\begin{lstlisting}
+For example, assume a caller can instantiates @N@ with 42 in the following (details to follow).
+\begin{cfa}
 forall( [N] )
 void declDemo() {
-	float a1[N];         // built-in type ("C array")
-	array(float, N) a2;  // type from library
-}
-\end{lstlisting}
-
-If a caller instantiates @N@ with 42, then both locally-declared array variables, @a1@ and @a2@, become arrays of 42 elements, each element being a @float@.
-The two variables have identical size and layout; they both encapsulate 42-float stack allocations, no heap allocations, and no further "bookkeeping" allocations/header.
-Having the @array@ library type (that of @a2@) is a tactical measure, an early implementation that offers full feature support.
-A future goal (TODO xref) is to port all of its features into the built-in array type (that of @a1@); then, the library type could be removed, and \CFA would have only one array type.
-In present state, the built-in array has partial support for the new features.
-The fully-featured library type is used exclusively in introductory examples; feature support and C compatibility are revisited in sec TODO.
-
-Offering the @array@ type, as a distinct alternative from the the C array, is consistent with \CFA's extension philosophy (TODO xref background) to date.
-A few compatibility-breaking changes to the behaviour of the C array were also made, both as an implementation convenience, and as justified fixes to C's lax treatment.
-
-The @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features.
-A clean slate was an important starting point because it meant not having to deal with every inherited complexity introduced in TODO xref background-array.
-
-
-My contributions are
-\begin{itemize}
-\item a type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@
+	float x1[N];				$\C{// built-in type ("C array")}$
+	array(float, N) x2;			$\C{// type from library}$
+}
+\end{cfa}
+Both of the locally-declared array variables, @x1@ and @x2@, have 42 elements, each element being a @float@.
+The two variables have identical size and layout; they both encapsulate 42-float, stack \vs heap allocations with no additional ``bookkeeping'' allocations or headers.
+Providing this explicit generic approach required a significant extension to the \CFA type system to support a full-feature, safe, efficient (space and time) array-type, which forms the foundation for more complex array forms in \CFA.
+
+Admittedly, the @array@ library type (type for @x2@) is syntactically different from its C counterpart.
+A future goal (TODO xref) is to provide a built-in array type with syntax approaching C's (type for @x1@);
+then, the library @array@ type can be removed giving \CFA a largely uniform array type.
+At present, the built-in array is only partially supported, so the generic @array@ is used exclusively in the discussion;
+feature support and C compatibility are revisited in Section ? TODO.
+
+Offering an @array@ type, as a distinct alternative to the C array, is consistent with \CFA's goal of backwards compatibility, \ie virtually all existing C (gcc) programs can be compiled by \CFA with only a small number of changes, similar to \CC (g++).
+However, a few compatibility-breaking changes to the behaviour of the C array are necessary, both as an implementation convenience and to fix C's lax treatment of arrays.
+Hence, the @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features, making it unnecessary to deal with every inherited complexity introduced by the C array TODO xref.
+
+My contributions are:
+\begin{enumerate}
+\item A type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@.
+\item Provide a length-checked array-type in the \CFA standard library, where the array's length is statically managed and dynamically valued.
+\item Provide argument/parameter passing safety for arrays and subscript safety.
 \item TODO: general parking...
-\item identify specific abilities brought by @array@
-\item Where there is a gap concerning this feature's readiness for prime-time, identification of specific workable improvements that are likely to close the gap
-\end{itemize}
+\item Identify the interesting specific abilities available by the new @array@ type.
+\item Where there is a gap concerning this feature's readiness for prime-time, identification of specific workable improvements that are likely to close the gap.
+\end{enumerate}
 
 
@@ -68,262 +70,401 @@
 
 
-\section{Features Added}
-
-The present work adds a type @array@ to the \CFA standard library~\cite{Cforall}.
-
-This array's length is statically managed and dynamically valued.
-This static management achieves argument safety and suggests a path to subscript safety as future work (TODO: cross reference).
-
-This section presents motivating examples of the new array type's usage and follows up with definitions of the notations that appear.
-
-The core of the new array management is tracking all array lengths in the type system.
-Dynamically valued lengths are represented using type variables.
-The stratification of type variables preceding object declarations makes a length referenceable everywhere that it is needed.
+\section{Features added}
+
+This section presents motivating examples for the new array type, demonstrating the syntax and semantics of the generic @array@.
+As stated, the core capability of the new array is tracking all dimensions in the type system, where dynamic dimensions are represented using type variables.
+
+The definition of type variables preceding object declarations makes the array dimension lexically referenceable where it is needed.
 For example, a declaration can share one length, @N@, among a pair of parameters and the return.
 \lstinput{10-17}{hello-array.cfa}
 Here, the function @f@ does a pointwise comparison, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
-
-The array type uses the parameterized length information in its @sizeof@ determination, illustrated in the example's call to @alloc@.
-That call requests an allocation of type @array(bool, N)@, which the type system deduces from the left-hand side of the initialization, into the return type of the @alloc@ call.
-Preexisting \CFA behaviour is leveraged here, both in the return-type-only polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine.
-The new @array@ type plugs into this behaviour by implementing the @sized@/@sizeof@ assertion to have the intuitive meaning.
-As a result, this design avoids an opportunity for programmer error by making the size/length communication to a called routine implicit, compared with C's @calloc@ (or the low-level \CFA analog @aalloc@), which take an explicit length parameter not managed by the type system.
-
-\VRef[Figure]{f:fHarness} shows the harness to use the @f@ function illustrating how dynamic values are fed into the system.
-Here, the @a@ array is loaded with decreasing values, and the @b@ array with amounts off by a constant, giving relative differences within tolerance at first and out of tolerance later.
-The program main is run with two different inputs of sequence length.
+The dynamic allocation of the @ret@ array by @alloc@ uses the parameterized dimension information in its implicit @_Alignof@ and @sizeof@ determinations, and casting the return type.
+\begin{cfa}
+static inline forall( T & | sized(T) )
+T * alloc( size_t dim ) {
+	if ( _Alignof(T) <= libAlign() ) return (T *)aalloc( dim, sizeof(T) ); // calloc without zero fill
+	else return (T *)amemalign( _Alignof(T), dim, sizeof(T) ); // array memalign
+}
+\end{cfa}
+Here, the type system deduces from the left-hand side of the assignment the type @array(bool, N)@, and forwards it as the type variable @T@ for the generic @alloc@ function, making it available in its body.
+Hence, preexisting \CFA behaviour is leveraged here, both in the return-type polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine.
+This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary @sized@ assertions needed by other types.
+(@sized@ implies a concrete \vs abstract type with a compile-time size.)
+As a result, there is significant programming safety by making the size accessible and implicit, compared with C's @calloc@ and non-array supporting @memalign@, which take an explicit length parameter not managed by the type system.
 
 \begin{figure}
-\lstinput{30-49}{hello-array.cfa}
+\lstinput{30-43}{hello-array.cfa}
+\lstinput{45-48}{hello-array.cfa}
 \caption{\lstinline{f} Harness}
 \label{f:fHarness}
 \end{figure}
 
-The loops in the program main follow the more familiar pattern of using the ordinary variable @n@ to convey the length.
-The type system implicitly captures this value at the call site (@main@ calling @f@) and makes it available within the callee (@f@'s loop bound).
-
-The two parts of the example show @n@ adapting a variable into a type-system managed length (at @main@'s declarations of @a@, @b@, and @result@), @N@ adapting in the opposite direction (at @f@'s loop bound), and a pass-thru use of a managed length (at @f@'s declaration of @ret@).
-
-The @forall( ...[N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and in the function @b@.
-The present form is chosen to parallel the existing @forall@ forms:
-\begin{cfa}
-forall( @[N]@ ) ... // array kind
-forall( & T  ) ...  // reference kind (dtype)
-forall( T  ) ...    // value kind (otype)
-\end{cfa}
-
-The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
+\VRef[Figure]{f:fHarness} shows a harness that uses the @f@ function illustrating how dynamic values are fed into the @array@ type.
+Here, the dimension of the @x@, @y@, and @result@ arrays is specified from a command-line value and these arrays are allocated on the stack.
+Then the @x@ array is initialized with decreasing values, and the @y@ array with amounts offset by constant @0.005@, giving relative differences within tolerance initially and diverging for later values.
+The program main is run (see figure bottom) with inputs @5@ and @7@ for sequence lengths.
+The loops follow the familiar pattern of using the variable @n@ to iterate through the arrays.
+Most importantly, the type system implicitly captures @n@ at the call of @f@ and makes it available throughout @f@ as @N@.
+The example shows @n@ adapting into a type-system managed length at the declarations of @x@, @y@, and @result@, @N@ adapting in the same way at @f@'s loop bound, and a pass-thru use of @n@ at @f@'s declaration of @ret@.
+Except for the lifetime-management issue of @result@, \ie explicit @free@, this program has eliminated both the syntactic and semantic problems associated with C arrays and their usage.
+These benefits cannot be underestimated.
+
+In general, the @forall( ..., [N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and within a function.
+The syntactic form is chosen to parallel other @forall@ forms:
+\begin{cfa}
+forall( @[N]@ ) ...	$\C[1.5in]{// array kind}$
+forall( T & ) ...	$\C{// reference kind (dtype)}$
+forall( T ) ...		$\C{// value kind (otype)}\CRT$
+\end{cfa}
+% The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
 In summary:
 \begin{itemize}
 \item
-@[N]@ -- within a forall, declares the type variable @N@ to be a managed length
-\item
-$e$ -- a type representing the value of $e$ as a managed length, where $e$ is a @size_t@-typed expression
-\item
-N -- an expression of type @size_t@, whose value is the managed length @N@
-\item
-@array( thing, N0, N1, ... )@ -- a type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects
+@[N]@ within a forall declares the type variable @N@ to be a managed length.
+\item
+The type of @N@ within code is @size_t@.
+\item
+The value of @N@ within code is the acquired length derived from the usage site, \ie generic declaration or function call.
+\item
+@array( thing, N0, N1, ... )@ is a multi-dimensional type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects.
 \end{itemize}
-Unsigned integers have a special status in this type system.
-Unlike how C++ allows
+
+\VRef[Figure]{f:TemplateVsGenericType} shows @N@ is not the same as a @size_t@ declaration in a \CC \lstinline[language=C++]{template}.
+\begin{enumerate}[leftmargin=*]
+\item
+The \CC template @N@ is a compile-time value, while the \CFA @N@ is a runtime value.
+\item
+The \CC template @N@ must be passed explicitly at the call, unless @N@ has a default value, even when \CC can deduct the type of @T@.
+The \CFA @N@ is part of the array type and passed implicitly at the call.
+\item
+\CC cannot have an array of references, but can have an array of pointers.
+\CC has a (mistaken) belief that references are not objects, but pointers are objects.
+In the \CC example, the arrays fall back on C arrays, which have a duality with references with respect to automatic dereferencing.
+The \CFA array is a contiguous object with an address, which can stored as a reference or pointer.
+\item
+C/\CC arrays cannot be copied, while \CFA arrays can be copied, making them a first-class object (although array copy is often avoided for efficiency).
+\end{enumerate}
+
+\begin{figure}
+\begin{tabular}{@{}l@{\hspace{20pt}}l@{}}
 \begin{c++}
-template< size_t N, char * msg, typename T >... // declarations
+
+@template< typename T, size_t N >@
+void copy( T ret[N], T x[N] ) {
+	for ( int i = 0; i < N; i += 1 ) ret[i] = x[i];
+}
+int main() {
+	int ret[10], x[10];
+	for ( int i = 0; i < 10; i += 1 ) x[i] = i;
+	@copy<int, 10 >( ret, x );@
+	for ( int i = 0; i < 10; i += 1 )
+		cout << ret[i] << ' ';
+	cout << endl;
+}
 \end{c++}
-\CFA does not accommodate values of any user-provided type.
-TODO: discuss connection with dependent types.
-An example of a type error demonstrates argument safety.
-The running example has @f@ expecting two arrays of the same length.
-A compile-time error occurs when attempting to call @f@ with arrays whose lengths may differ.
-\begin{cfa}
-forall( [M], [N] )
-void bad( array(float, M) &a, array(float, N) &b ) {
-	f( a, a ); // ok
-	f( b, b ); // ok
-	f( a, b ); // error
-}
-\end{cfa}
-%\lstinput{60-65}{hello-array.cfa}
-As is common practice in C, the programmer is free to cast, to assert knowledge not shared with the type system.
-\begin{cfa}
-forall( [M], [N] )
-void bad_fixed( array(float, M) & a, array(float, N) & b ) {
-	if ( M == N ) {
-	    f( a, (array(float, M) &)b ); // cast b to matching type
+&
+\begin{cfa}
+int main() {
+	@forall( T, [N] )@   // nested function
+	void copy( array( T, N ) & ret, array( T, N ) & x ) {
+		for ( i; 10 ) ret[i] = x[i];
 	}
-}
-\end{cfa}
-%\lstinput{70-75}{hello-array.cfa}
-
-Argument safety and the associated implicit communication of array length work with \CFA's generic types too.
-\CFA allows aggregate types to be generalized with multiple type parameters, including parameterized element type, so can it be defined over a parameterized length.
-Doing so gives a refinement of C's ``flexible array member'' pattern, that allows nesting structures with array members anywhere within other structures.
-\lstinput{10-16}{hello-accordion.cfa}
-This structure's layout has the starting offset of @cost_contribs@ varying in @Nclients@, and the offset of @total_cost@ varying in both generic parameters.
-For a function that operates on a @request@ structure, the type system handles this variation transparently.
-\lstinput{40-47}{hello-accordion.cfa}
-In the example, different runs of the program result in different offset values being used.
-\lstinput{60-76}{hello-accordion.cfa}
+
+	array( int, 10 ) ret, x;
+	for ( i; 10 ) x[i] = i;
+	@copy( ret,  x );@
+	for ( i; 10 )
+		sout | ret[i] | nonl;
+	sout | nl;
+}
+\end{cfa}
+\end{tabular}
+\caption{\CC \lstinline[language=C++]{template} \vs \CFA generic type }
+\label{f:TemplateVsGenericType}
+\end{figure}
+
+Continuing the discussion of \VRef[Figure]{f:fHarness}, the example has @f@ expecting two arrays of the same length.
+A compile-time error occurs when attempting to call @f@ with arrays of differing lengths.
+% removing leading whitespace
+\lstinput[tabsize=1]{52-53}{hello-array.cfa}
+\lstinput[tabsize=1,aboveskip=0pt]{62-64}{hello-array.cfa}
+As is common practice in C, the programmer is free to cast, \ie to assert knowledge not shared with the type system.
+\lstinput{70-74}{hello-array.cfa}
+
+Orthogonally, the new @array@ type works with \CFA's generic types, providing argument safety and the associated implicit communication of array length.
+Specifically, \CFA allows aggregate types to be generalized with multiple type parameters, including parameterized element types and lengths.
+Doing so gives a refinement of C's ``flexible array member'' pattern, allowing nesting structures with array members anywhere within other structures.
+\lstinput{10-15}{hello-accordion.cfa}
+This structure's layout has the starting offset of @municipalities@ varying in @NprovTerty@, and the offset of @total_pt@ and @total_mun@ varying in both generic parameters.
+For a function that operates on a @CanadaPop@ structure, the type system handles this variation transparently.
+\lstinput{40-45}{hello-accordion.cfa}
+\VRef[Figure]{f:checkHarness} shows program results where different offset values being used.
 The output values show that @summarize@ and its caller agree on both the offsets (where the callee starts reading @cost_contribs@ and where the callee writes @total_cost@).
-Yet the call site still says just, ``pass the request.''
-
-
-\section{Multidimensional implementation}
+Yet the call site just says, ``pass the request.''
+
+\begin{figure}
+\lstinput{60-68}{hello-accordion.cfa}
+\lstinput{70-72}{hello-accordion.cfa}
+\caption{\lstinline{check} Harness}
+\label{f:checkHarness}
+\end{figure}
+
+
+\section{Multidimensional Arrays}
 \label{toc:mdimpl}
 
-TODO: introduce multidimensional array feature and approaches
-
-The new \CFA standard library @array@ datatype supports multidimensional uses more richly than the C array.
-The new array's multidimensional interface and implementation, follows an array-of-arrays setup, meaning, like C's @float[n][m]@ type, one contiguous object, with coarsely-strided dimensions directly wrapping finely-strided dimensions.
-This setup is in contrast with the pattern of array of pointers to other allocations representing a sub-array.
-Beyond what C's type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order.
-C and C++ require a programmer with such a need to manage pointer/offset arithmetic manually.
-
-Examples are shown using a $5 \times 7$ float array, @a@, loaded with increments of $0.1$ when stepping across the length-7 finely-strided dimension shown on columns, and with increments of $1.0$ when stepping across the length-5 coarsely-strided dimension shown on rows.
-%\lstinput{120-126}{hello-md.cfa}
-The memory layout of @a@ has strictly increasing numbers along its 35 contiguous positions.
+% TODO: introduce multidimensional array feature and approaches
+
+When working with arrays, \eg linear algebra, array dimensions are referred to as ``rows'' and ``columns'' for a matrix, adding ``planes'' for a cube.
+(There is little terminology for higher dimensional arrays.)
+For example, an acrostic poem\footnote{A type of poetry where the first, last or other letters in a line spell out a particular word or phrase in a vertical column.}
+can be treated as a grid of characters, where the rows are the text and the columns are the embedded keyword(s).
+Within a poem, there is the concept of a \newterm{slice}, \eg a row is a slice for the poem text, a column is a slice for a keyword.
+In general, the dimensioning and subscripting for multidimensional arrays has two syntactic forms: @m[r,c]@ or @m[r][c]@.
+
+Commonly, an array, matrix, or cube, is visualized (especially in mathematics) as a contiguous row, rectangle, or block.
+This conceptualization is reenforced by subscript ordering, \eg $m_{r,c}$ for a matrix and $c_{p,r,c}$ for a cube.
+Few programming languages differ from the mathematical subscript ordering.
+However, computer memory is flat, and hence, array forms are structured in memory as appropriate for the runtime system.
+The closest representation to the conceptual visualization is for an array object to be contiguous, and the language structures this memory using pointer arithmetic to access the values using various subscripts.
+This approach still has degrees of layout freedom, such as row or column major order, \ie juxtaposed rows or columns in memory, even when the subscript order remains fixed.
+For example, programming languages like MATLAB, Fortran, Julia and R store matrices in column-major order since they are commonly used for processing column-vectors in tabular data sets but retain row-major subscripting.
+In general, storage layout is hidden by subscripting, and only appears when passing arrays among different programming languages or accessing specific hardware.
+
+\VRef[Figure]{f:FixedVariable} shows two C90 approaches for manipulating contiguous arrays.
+Note, C90 does not support VLAs.
+The fixed-dimension approach uses the type system;
+however, it requires all dimensions except the first to be specified at compile time, \eg @m[][6]@, allowing all subscripting stride calculations to be generated with constants.
+Hence, every matrix passed to @fp1@ must have exactly 6 columns but the row size can vary.
+The variable-dimension approach ignores (violates) the type system, \ie argument and parameters types do not match, and manually performs pointer arithmetic for subscripting in the macro @sub@.
+
+\begin{figure}
+\begin{tabular}{@{}l@{\hspace{40pt}}l@{}}
+\multicolumn{1}{c}{\textbf{Fixed Dimension}} & \multicolumn{1}{c}{\textbf{Variable Dimension}} \\
+\begin{cfa}
+
+void fp1( int rows, int m[][@6@] ) {
+	...  printf( "%d ", @m[r][c]@ );  ...
+}
+int fm1[4][@6@], fm2[6][@6@]; // no VLA
+// initialize matrixes
+fp1( 4, fm1 ); // implicit 6 columns
+fp1( 6, fm2 );
+\end{cfa}
+&
+\begin{cfa}
+#define sub( m, r, c ) *(m + r * sizeof( m[0] ) + c)
+void fp2( int rows, int cols, int *m ) {
+	...  printf( "%d ", @sub( m, r, c )@ );  ...
+}
+int vm1[4][4], vm2[6][8]; // no VLA
+// initialize matrixes
+fp2( 4, 4, vm1 );
+fp2( 6, 8, vm2 );
+\end{cfa}
+\end{tabular}
+\caption{C90 Fixed \vs Variable Contiguous Matrix Styles}
+\label{f:FixedVariable}
+\end{figure}
+
+Many languages allow multidimensional arrays-of-arrays, \eg in Pascal or \CC.
+\begin{cquote}
+\begin{tabular}{@{}ll@{}}
+\begin{pascal}
+var m : array[0..4, 0..4] of Integer;  (* matrix *)
+type AT = array[0..4] of Integer;  (* array type *)
+type MT = array[0..4] of AT;  (* array of array type *)
+var aa : MT;  (* array of array variable *)
+m@[1][2]@ := 1;   aa@[1][2]@ := 1 (* same subscripting *)
+\end{pascal}
+&
+\begin{c++}
+int m[5][5];
+
+typedef vector< vector<int> > MT;
+MT vm( 5, vector<int>( 5 ) );
+m@[1][2]@ = 1;  aa@[1][2]@ = 1;
+\end{c++}
+\end{tabular}
+\end{cquote}
+The language decides if the matrix and array-of-array are laid out the same or differently.
+For example, an array-of-array may be an array of row pointers to arrays of columns, so the rows may not be contiguous in memory nor even the same length (triangular matrix).
+Regardless, there is usually a uniform subscripting syntax masking the memory layout, even though the two array forms could be differentiated at the subscript level, \eg @m[1,2]@ \vs @aa[1][2]@.
+Nevertheless, controlling memory layout can make a difference in what operations are allowed and in performance (caching/NUMA effects).
+
+C also provides non-contiguous arrays-of-arrays.
+\begin{cfa}
+int m[5][5];							$\C{// contiguous}$
+int * aa[5];							$\C{// non-contiguous}$
+\end{cfa}
+both with different memory layout using the same subscripting, and both with different degrees of issues.
+The focus of this work is on the contiguous multidimensional arrays in C.
+The reason is that programmers are often forced to use the more complex array-of-array form when a contiguous array would be simpler, faster, and safer.
+Nevertheless, the C array-of-array form continues to be useful for special circumstances.
+
+\VRef[Figure]{f:ContiguousNon-contiguous} shows the extensions made in C99 for manipulating contiguous \vs non-contiguous arrays.\footnote{C90 also supported non-contiguous arrays.}
+First, VLAs are supported.
+Second, for contiguous arrays, C99 conjoins one or more of the parameters as a downstream dimension(s), \eg @cols@, implicitly using this parameter to compute the row stride of @m@.
+If the declaration of @fc@ is changed to:
+\begin{cfa}
+void fc( int rows, int cols, int m[@rows@][@cols@] ) ...
+\end{cfa}
+it is possible for C to perform bound checking across all subscripting, but it does not.
+While this contiguous-array capability is a step forward, it is still the programmer's responsibility to manually manage the number of dimensions and their sizes, both at the function definition and call sites.
+That is, the array does not automatically carry its structure and sizes for use in computing subscripts.
+While the non-contiguous style in @faa@ looks very similar to @fc@, the compiler only understands the unknown-sized array of row pointers, and it relies on the programmer to traverse the columns in a row correctly.
+Specifically, there is no requirement that the rows are the same length, like a poem with different length lines.
+
+\begin{figure}
+\begin{tabular}{@{}ll@{}}
+\multicolumn{1}{c}{\textbf{Contiguous}} & \multicolumn{1}{c}{\textbf{ Non-contiguous}} \\
+\begin{cfa}
+void fc( int rows, @int cols@, int m[ /* rows */ ][@cols@] ) {
+	...  printf( "%d ", @m[r][c]@ );  ...
+}
+int m@[5][5]@;
+for ( int r = 0; r < 5; r += 1 ) {
+
+	for ( int c = 0; c < 5; c += 1 )
+		m[r][c] = r + c;
+}
+fc( 5, 5, m );
+\end{cfa}
+&
+\begin{cfa}
+void faa( int rows, int cols, int * m[ @/* cols */@ ] ) {
+	...  printf( "%d ", @m[r][c]@ );  ...
+}
+int @* aa[5]@;  // row pointers
+for ( int r = 0; r < 5; r += 1 ) {
+	@aa[r] = malloc( 5 * sizeof(int) );@ // create rows
+	for ( int c = 0; c < 5; c += 1 )
+		aa[r][c] = r + c;
+}
+faa( 5, 5, aa );
+\end{cfa}
+\end{tabular}
+\caption{C99 Contiguous \vs Non-contiguous Matrix Styles}
+\label{f:ContiguousNon-contiguous}
+\end{figure}
+
+
+\subsection{Multidimensional array implementation}
+
+A multidimensional array implementation has three relevant levels of abstraction, from highest to lowest, where the array occupies \emph{contiguous memory}.
+\begin{enumerate}
+\item
+Flexible-stride memory:
+this model has complete independence between subscripting ordering and memory layout, offering the ability to slice by (provide an index for) any dimension, \eg slice a plane, row, or column, \eg @c[3][*][*]@, @c[3][4][*]@, @c[3][*][5]@.
+\item
+Fixed-stride memory:
+this model binds the first subscript and the first memory layout dimension, offering the ability to slice by (provide an index for) only the coarsest dimension, @m[row][*]@ or @c[plane][*][*]@, \eg slice only by row (2D) or plane (3D).
+After which, subscripting and memory layout are independent.
+\item
+Explicit-displacement memory:
+this model has no awareness of dimensions just the ability to access memory at a distance from a reference point (base-displacement addressing), \eg @x + 23@ or @x[23}@ $\Rightarrow$ 23rd element from the start of @x@.
+A programmer must manually build any notion of dimensions using other tools;
+hence, this style is not offering multidimensional arrays \see{\VRef[Figure]{f:FixedVariable}}.
+\end{enumerate}
+
+There is some debate as to whether the abstraction ordering goes $\{1, 2\} < 3$, rather than my numerically-ordering.
+That is, styles 1 and 2 are at the same abstraction level, with 3 offering a limited set of functionality.
+I chose to build the \CFA style-1 array upon a style-2 abstraction.
+(Justification of the decision follows, after the description of the design.)
+
+Style 3 is the inevitable target of any array implementation.
+The hardware offers this model to the C compiler, with bytes as the unit of displacement.
+C offers this model to its programmer as pointer arithmetic, with arbitrary sizes as the unit.
+Casting a multidimensional array as a single-dimensional array/pointer, then using @x[i]@ syntax to access its elements, is still a form of pointer arithmetic.
+
+Now stepping into the implementation of \CFA's new type-1 multidimensional arrays in terms of C's existing type-2 multidimensional arrays, it helps to clarify that even the interface is quite low-level.
+A C/\CFA array interface includes the resulting memory layout.
+The defining requirement of a type-2 system is the ability to slice a column from a column-finest matrix.
+The required memory shape of such a slice is set, before any discussion of implementation.
+The implementation presented here is how the \CFA array library wrangles the C type system, to make it do memory steps that are consistent with this layout.
+TODO: do I have/need a presentation of just this layout, just the semantics of -[all]?
+
+The new \CFA standard library @array@ datatype supports richer multidimensional features than C.
+The new array implementation follows C's contiguous approach, \ie @float [r][c]@, with one contiguous object subscripted by coarsely-strided dimensions directly wrapping finely-strided dimensions.
+Beyond what C's array type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order.
+
+The following examples use an @array( float, 5, 7) m@, loaded with values incremented by $0.1$, when stepping across the length-7 finely-strided column dimension, and stepping across the length-5 coarsely-strided row dimension.
+\par\noindent
+\mbox{\lstinput{121-126}{hello-md.cfa}}
+\par\noindent
+The memory layout is 35 contiguous elements with strictly increasing addresses.
 
 A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays.
-Like with the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array, by a prefix of its dimensions.
-This action first subscripts away the most coarsely strided dimensions, leaving a result that expects to be be subscripted by the more finely strided dimensions.
-\lstinput{60-66}{hello-md.cfa}
+As for the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array by a prefix of its dimensions, \eg @m[2]@, giving the third row.
+This action first subscripts away the most coarsely strided dimensions, leaving a result that expects to be subscripted by the more finely strided dimensions, \eg @m[2][3]@, giving the value @2.3@.
+The following is an example slicing a row.
+\lstinput{60-64}{hello-md.cfa}
 \lstinput[aboveskip=0pt]{140-140}{hello-md.cfa}
 
-This function declaration is asserting too much knowledge about its parameter @c@, for it to be usable for printing either a row slice or a column slice.
-Specifically, declaring the parameter @c@ with type @array@ means that @c@ is contiguous.
-However, the function does not use this fact.
-For the function to do its job, @c@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@), with managed length @N@.
+However, function @print1d@ is asserting too much knowledge about its parameter @r@ for printing either a row slice or a column slice.
+Specifically, declaring the parameter @r@ with type @array@ means that @r@ is contiguous, which is unnecessarily restrictive.
+That is, @r@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@) with managed length @N@.
 The new-array library provides the trait @ix@, so-defined.
-With it, the original declaration can be generalized, while still implemented with the same body, to the latter declaration:
-\lstinput{40-44}{hello-md.cfa}
+With it, the original declaration can be generalized with the same body.
+\lstinput{43-44}{hello-md.cfa}
 \lstinput[aboveskip=0pt]{145-145}{hello-md.cfa}
-
-Nontrivial slicing, in this example, means passing a noncontiguous slice to @print1d@.
-The new-array library provides a ``subscript by all'' operation for this purpose.
-In a multi-dimensional subscript operation, any dimension given as @all@ is left ``not yet subscripted by a value,'' implementing the @ix@ trait, waiting for such a value.
+The nontrivial slicing in this example now allows passing a \emph{noncontiguous} slice to @print1d@, where the new-array library provides a ``subscript by all'' operation for this purpose.
+In a multi-dimensional subscript operation, any dimension given as @all@ is a placeholder, \ie ``not yet subscripted by a value'', waiting for such a value, implementing the @ix@ trait.
 \lstinput{150-151}{hello-md.cfa}
 
-The example has shown that @a[2]@ and @a[[2, all]]@ both refer to the same, ``2.*'' slice.
-Indeed, the various @print1d@ calls under discussion access the entry with value 2.3 as @a[2][3]@, @a[[2,all]][3]@, and @a[[all,3]][2]@.
-This design preserves (and extends) C array semantics by defining @a[[i,j]]@ to be @a[i][j]@ for numeric subscripts, but also for ``subscripting by all''.
+The example shows @x[2]@ and @x[[2, all]]@ both refer to the same, ``2.*'' slice.
+Indeed, the various @print1d@ calls under discussion access the entry with value @2.3@ as @x[2][3]@, @x[[2,all]][3]@, and @x[[all,3]][2]@.
+This design preserves (and extends) C array semantics by defining @x[[i,j]]@ to be @x[i][j]@ for numeric subscripts, but also for ``subscripting by all''.
 That is:
-
-\begin{tabular}{cccccl}
-@a[[2,all]][3]@  &  $=$  &  @a[2][all][3]@  & $=$  &  @a[2][3]@  & (here, @all@ is redundant)  \\
-@a[[all,3]][2]@  &  $=$  &  @a[all][3][2]@  & $=$  &  @a[2][3]@  & (here, @all@ is effective)
+\begin{cquote}
+\begin{tabular}{@{}cccccl@{}}
+@x[[2,all]][3]@	& $\equiv$	& @x[2][all][3]@  & $\equiv$	& @x[2][3]@  & (here, @all@ is redundant)  \\
+@x[[all,3]][2]@	& $\equiv$	& @x[all][3][2]@  & $\equiv$	& @x[2][3]@  & (here, @all@ is effective)
 \end{tabular}
-
-Narrating progress through each of the @-[-][-][-]@ expressions gives, firstly, a definition of @-[all]@, and secondly, a generalization of C's @-[i]@.
-
-\noindent Where @all@ is redundant:
-
-\begin{tabular}{ll}
-@a@  & 2-dimensional, want subscripts for coarse then fine \\
-@a[2]@  & 1-dimensional, want subscript for fine; lock coarse = 2 \\
-@a[2][all]@  & 1-dimensional, want subscript for fine \\
-@a[2][all][3]@  & 0-dimensional; lock fine = 3
+\end{cquote}
+
+Narrating progress through each of the @-[-][-][-]@\footnote{
+The first ``\lstinline{-}'' is a variable expression and the remaining ``\lstinline{-}'' are subscript expressions.}
+expressions gives, firstly, a definition of @-[all]@, and secondly, a generalization of C's @-[i]@.
+Where @all@ is redundant:
+\begin{cquote}
+\begin{tabular}{@{}ll@{}}
+@x@  & 2-dimensional, want subscripts for coarse then fine \\
+@x[2]@  & 1-dimensional, want subscript for fine; lock coarse == 2 \\
+@x[2][all]@  & 1-dimensional, want subscript for fine \\
+@x[2][all][3]@  & 0-dimensional; lock fine == 3
 \end{tabular}
-
-\noindent Where @all@ is effective:
-
-\begin{tabular}{ll}
-@a@  & 2-dimensional, want subscripts for coarse then fine \\
-@a[all]@  & 2-dimensional, want subscripts for fine then coarse \\
-@a[all][3]@  & 1-dimensional, want subscript for coarse; lock fine = 3 \\
-@a[all][3][2]@  & 0-dimensional; lock coarse = 2
+\end{cquote}
+Where @all@ is effective:
+\begin{cquote}
+\begin{tabular}{@{}ll@{}}
+@x@  & 2-dimensional, want subscripts for coarse then fine \\
+@x[all]@  & 2-dimensional, want subscripts for fine then coarse \\
+@x[all][3]@  & 1-dimensional, want subscript for coarse; lock fine == 3 \\
+@x[all][3][2]@  & 0-dimensional; lock coarse == 2
 \end{tabular}
-
+\end{cquote}
 The semantics of @-[all]@ is to dequeue from the front of the ``want subscripts'' list and re-enqueue at its back.
+For example, in a two dimensional matrix, this semantics conceptually transposes the matrix by reversing the subscripts.
 The semantics of @-[i]@ is to dequeue from the front of the ``want subscripts'' list and lock its value to be @i@.
 
-Contiguous arrays, and slices of them, are all realized by the same underlying parameterized type.
-It includes stride information in its metatdata.
-The @-[all]@ operation is a conversion from a reference to one instantiation, to a reference to another instantiation.
+Contiguous arrays, and slices of them, are all represented by the same underlying parameterized type, which includes stride information in its metatdata.
+\PAB{Do not understand this sentence: The \lstinline{-[all]} operation is a conversion from a reference to one instantiation to a reference to another instantiation.}
 The running example's @all@-effective step, stated more concretely, is:
-
-\begin{tabular}{ll}
-@a@       & : 5 of ( 7 of float each spaced 1 float apart ) each spaced 7 floats apart \\
-@a[all]@  & : 7 of ( 5 of float each spaced 7 floats apart ) each spaced 1 float apart
+\begin{cquote}
+\begin{tabular}{@{}ll@{}}
+@x@       & : 5 of ( 7 of @float@ each spaced 1 @float@ apart ) each spaced 7 @floats@ apart \\
+@x[all]@  & : 7 of ( 5 of @float@ each spaced 7 @float@s apart ) each spaced 1 @float@ apart
 \end{tabular}
+\end{cquote}
 
 \begin{figure}
 \includegraphics{measuring-like-layout}
-\caption{Visualization of subscripting, by numeric value, and by \lstinline[language=CFA]{all}.
-	Here \lstinline[language=CFA]{x} has type \lstinline[language=CFA]{array( float, 5, 7 )}, understood as 5 rows by 7 columns.
-	The horizontal layout represents contiguous memory addresses while the vertical layout uses artistic license.
-	The vertical shaded band highlights the location of the targeted element, 2.3.
-	Any such vertical contains various interpretations of a single address.}
+\caption{Visualization of subscripting by value and by \lstinline[language=CFA]{all}, for \lstinline{x} of type \lstinline{array( float, 5, 7 )} understood as 5 rows by 7 columns.
+The horizontal layout represents contiguous memory addresses while the vertical layout is conceptual.
+The vertical shaded band highlights the location of the targeted element, 2.3.
+Any such vertical slice contains various interpretations of a single address.}
 \label{fig:subscr-all}
 \end{figure}
-
-\noindent BEGIN: Paste looking for a home
-
-The world of multidimensional array implementation has, or abuts, four relevant levels of abstraction, highest to lowest:
-
-1, purpose:
-If you are doing linear algebra, you might call its dimensions, "column" and "row."
-If you are treating an acrostic poem as a grid of characters, you might say,
-the direction of reading the phrases vs the direction of reading the keyword.
-
-2, flexible-stride memory:
-assuming, from here on, a need to see/use contiguous memory,
-this model offers the ability to slice by (provide an index for) any dimension
-
-3, fixed-stride memory:
-this model offers the ability to slice by (provide an index for) only the coarsest dimension
-
-4, explicit-displacement memory:
-no awareness of dimensions, so no distinguishing them; just the ability to access memory at a distance from a reference point
-
-C offers style-3 arrays.  Fortran, Matlab and APL offer style-2 arrays.
-Offering style-2 implies offering style-3 as a sub-case.
-My CFA arrays are style-2.
-
-Some debate is reasonable as to whether the abstraction actually goes $ 1 < \{2, 3\} < 4 $,
-rather than my numerically-ordered chain.
-According to the diamond view, styles 2 and 3 are at the same abstraction level, just with 3 offering a more limited set of functionality.
-The chain view reflects the design decision I made in my mission to offer a style-2 abstraction;
-I chose to build it upon a style-3 abstraction.
-(Justification of the decision follows, after the description of the design.)
-
-The following discussion first dispenses with API styles 1 and 4, then elaborates on my work with styles 2 and 3.
-
-Style 1 is not a concern of array implementations.
-It concerns documentation and identifier choices of the purpose-specific API.
-If one is offering a matrix-multiply function, one must specify which dimension(s) is/are being summed over
-(or rely on the familiar convention of these being the first argument's rows and second argument's columns).
-Some libraries offer a style-1 abstraction that is not directly backed by a single array
-(e.g. make quadrants contiguous, as may help cache coherence during a parallel matrix multiply),
-but such designs are out of scope for a discussion on arrays; they are applications of several arrays.
-I typically include style-1 language with examples to help guide intuition.
-
-It is often said that C has row-major arrays while Fortran has column-major arrays.
-This comparison brings an unhelpful pollution of style-1 thinking into issues of array implementation.
-Unfortunately, ``-major'' has two senses: the program's order of presenting indices and the array's layout in memory.
-(The program's order could be either lexical, as in @x[1,2,3]@ subscripting, or runtime, as in the @x[1][2][3]@ version.)
-Style 2 is concerned with introducing a nontrivial relationship between program order and memory order,
-while style 3 sees program order identical with memory order.
-Both C and (the style-3 subset of) Fortran actually use the same relationship here:
-an earlier subscript in program order controls coarser steps in memory.
-The job of a layer-2/3 system is to implement program-ordered subscripting according to a defined memory layout.
-C and Fortran do not use opposite orders in doing this job.
-Fortran is only ``backward'' in its layer-1 conventions for reading/writing and linear algebra.
-Fortran subscripts as $m(c,r)$.  When I use style-1 language, I am following the C/mathematical convention of $m(r,c)$.
-
-Style 4 is the inevitable target of any array implementation.
-The hardware offers this model to the C compiler, with bytes as the unit of displacement.
-C offers this model to its programmer as pointer arithmetic, with arbitrary sizes as the unit.
-I consider casting a multidimensional array as a single-dimensional array/pointer,
-then using @x[i]@ syntax to access its elements, to be a form of pointer arithmetic.
-But style 4 is not offering arrays.
-
-Now stepping into the implementation
-of CFA's new type-3 multidimensional arrays in terms of C's existing type-2 multidimensional arrays,
-it helps to clarify that even the interface is quite low-level.
-A C/CFA array interface includes the resulting memory layout.
-The defining requirement of a type-3 system is the ability to slice a column from a column-finest matrix.
-The required memory shape of such a slice is set, before any discussion of implementation.
-The implementation presented here is how the CFA array library wrangles the C type system,
-to make it do memory steps that are consistent with this layout.
-TODO: do I have/need a presentation of just this layout, just the semantics of -[all]?
 
 Figure~\ref{fig:subscr-all} shows one element (in the shaded band) accessed two different ways: as @x[2][3]@ and as @x[all][3][2]@.
@@ -365,5 +506,5 @@
 The subscript operator presents what's really inside, by casting to the type below the wedge of lie.
 
-%  Does x[all] have to lie too?  The picture currently glosses over how it it advertizes a size of 7 floats.  I'm leaving that as an edge case benignly misrepresented in the picture.  Edge cases only have to be handled right in the code.
+%  Does x[all] have to lie too?  The picture currently glosses over how it it advertises a size of 7 floats.  I'm leaving that as an edge case benignly misrepresented in the picture.  Edge cases only have to be handled right in the code.
 
 Casting, overlapping and lying are unsafe.
@@ -392,20 +533,19 @@
 
 The @arpk@ structure and its @-[i]@ operator are thus defined as:
-\begin{lstlisting}
-forall( ztype(N),               // length of current dimension
-	dtype(S) | sized(S),    // masquerading-as
-	dtype E_im,             // immediate element, often another array
-	dtype E_base            // base element, e.g. float, never array
- ) {
-struct arpk {
-	S strides[N];           // so that sizeof(this) is N of S
-};
-
-// expose E_im, stride by S
-E_im & ?[?]( arpk(N, S, E_im, E_base) & a, ptrdiff_t i ) {
-	return (E_im &) a.strides[i];
-}
-}
-\end{lstlisting}
+\begin{cfa}
+forall( ztype(N),			$\C{// length of current dimension}$
+	dtype(S) | sized(S),	$\C{// masquerading-as}$
+	dtype E_im,				$\C{// immediate element, often another array}$
+	dtype E_base			$\C{// base element, e.g. float, never array}$
+) { // distribute forall to each element
+	struct arpk {
+		S strides[N];		$\C{// so that sizeof(this) is N of S}$
+	};
+	// expose E_im, stride by S
+	E_im & ?[?]( arpk(N, S, E_im, E_base) & a, ptrdiff_t i ) {
+		return (E_im &) a.strides[i];
+	}
+}
+\end{cfa}
 
 An instantiation of the @arpk@ generic is given by the @array(E_base, N0, N1, ...)@ expansion, which is @arpk( N0, Rec, Rec, E_base )@, where @Rec@ is @array(E_base, N1, ...)@.
@@ -464,25 +604,25 @@
 
 \begin{tabular}{rl}
-C      &  @void f( size_t n, size_t m, float a[n][m] );@ \\
+C      &  @void f( size_t n, size_t m, float x[n][m] );@ \\
 Java   &  @void f( float[][] a );@
 \end{tabular}
 
-Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access.
+Java's safety against undefined behaviour assures the callee that, if @x@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @x[i]@ is a valid access.
 If a value of @i@ outside this range is used, a runtime error is guaranteed.
 In these respects, C offers no guarantees at all.
-Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only.
-Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention.
-Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error.
+Notably, the suggestion that @n@ is the intended size of the first dimension of @x@ is documentation only.
+Indeed, many might prefer the technically equivalent declarations @float x[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention.
+Moreover, even if @x[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @x[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error.
 
 Java's lack of expressiveness for more applied properties means these outcomes are possible:
 \begin{itemize}
-\item @a[0][17]@ and @a[2][17]@ are valid accesses, yet @a[1][17]@ is a runtime error, because @a[1]@ is a null pointer
-\item the same observation, now because @a[1]@ refers to an array of length 5
-\item execution times vary, because the @float@ values within @a@ are sometimes stored nearly contiguously, and other times, not at all
+\item @x[0][17]@ and @x[2][17]@ are valid accesses, yet @x[1][17]@ is a runtime error, because @x[1]@ is a null pointer
+\item the same observation, now because @x[1]@ refers to an array of length 5
+\item execution times vary, because the @float@ values within @x@ are sometimes stored nearly contiguously, and other times, not at all
 \end{itemize}
 C's array has none of these limitations, nor do any of the ``array language'' comparators discussed in this section.
 
 This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [TODO:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array.
-The advice is that, while a vector is also more powerful (and quirky) than an array, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors.
+The advice is that, while a vector is also more powerful (and quirky) than an array, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @x[i]@), to avoid using @push_back@, and to use a vector of vectors.
 Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values.
 Allowing this scheme the same referential integrity assumption that \CFA enjoys [TODO:xref], this scheme matches Java's safety and expressiveness exactly.
@@ -532,5 +672,5 @@
 Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not.
 
-CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances.
+\CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances.
 Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark.
 Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.
@@ -539,5 +679,5 @@
 
 
-\section{Future Work}
+\section{Future work}
 
 \subsection{Declaration syntax}
@@ -553,5 +693,5 @@
 I will not discuss the core of this project, which has a tall mission already, to improve type safety, maintain appropriate C compatibility and offer more flexibility about storage use.
 It also has a candidate stretch goal, to adapt \CFA's @forall@ generic system to communicate generalized enumerations:
-\begin{lstlisting}
+\begin{cfa}
 forall( T | is_enum(T) )
 void show_in_context( T val ) {
@@ -565,7 +705,7 @@
 enum weekday { mon, tue, wed = 500, thu, fri };
 show_in_context( wed );
-\end{lstlisting}
+\end{cfa}
 with output
-\begin{lstlisting}
+\begin{cfa}
 mon
 tue < ready
@@ -573,5 +713,5 @@
 thu
 fri
-\end{lstlisting}
+\end{cfa}
 The details in this presentation aren't meant to be taken too precisely as suggestions for how it should look in \CFA.
 But the example shows these abilities:
@@ -599,10 +739,10 @@
 The structural assumptions required for the domain of an array in Dex are given by the trait (there, ``interface'') @Ix@, which says that the parameter @n@ is a type (which could take an argument like @weekday@) that provides two-way conversion with the integers and a report on the number of values.
 Dex's @Ix@ is analogous the @is_enum@ proposed for \CFA above.
-\begin{lstlisting}
+\begin{cfa}
 interface Ix n
- get_size n : Unit -> Int
- ordinal : n -> Int
- unsafe_from_ordinal n : Int -> n
-\end{lstlisting}
+get_size n : Unit -> Int
+ordinal : n -> Int
+unsafe_from_ordinal n : Int -> n
+\end{cfa}
 
 Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes.
@@ -616,18 +756,18 @@
 In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $.
 This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements
-\begin{lstlisting}
+\begin{cfa}
 instance {a b} [Ix a, Ix b] Ix (a & b)
- get_size = \(). size a * size b
- ordinal = \(i, j). (ordinal i * size b) + ordinal j
- unsafe_from_ordinal = \o.
+get_size = \(). size a * size b
+ordinal = \(i, j). (ordinal i * size b) + ordinal j
+unsafe_from_ordinal = \o.
 bs = size b
 (unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs))
-\end{lstlisting}
+\end{cfa}
 and by a user-provided adapter expression at the call site that shows how to indexing with a tuple is backed by indexing each dimension at a time
-\begin{lstlisting}
+\begin{cfa}
 img_trans :: (img_wd,img_ht)=>Real
 img_trans.(i,j) = img.i.j
 result = pairwise img_trans
-\end{lstlisting}
+\end{cfa}
 [TODO: cite as simplification of example from https://openreview.net/pdf?id=rJxd7vsWPS section 4]
 
@@ -661,5 +801,5 @@
 void * malloc( size_t );
 // C, user
-struct tm * el1 = malloc(      sizeof(struct tm) );
+struct tm * el1 = malloc( sizeof(struct tm) );
 struct tm * ar1 = malloc( 10 * sizeof(struct tm) );