Index: doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
@@ -0,0 +1,58 @@
+#include <stdio.h>
+#include <assert.h>
+#include <stdlib.h>
+
+#ifdef ERRS
+#define ERR(...) __VA_ARGS__
+#else
+#define ERR(...)
+#endif
+
+int main() {
+
+/*
+    These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
+*/
+    float * x;         // x points at a floating-point number
+    void (*y)(void);   // y points at a function
+                       ERR(
+    x = y;             // wrong
+    y = x;             // wrong
+                       )
+
+/*
+    The first gets
+        warning: assignment to `float *' from incompatible pointer type `void (*)(void)'
+    and the second gets the opposite.
+
+    Similarly,
+*/
+
+    float pi = 3.14;
+    void f( void (*g)(void) ) {
+        g();
+    }
+                       ERR(
+    f( & pi );         // wrong
+                       )
+/*
+    gets
+        warning: passing argument 1 of `f' from incompatible pointer type
+    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
+*/
+
+}
Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
@@ -0,0 +1,204 @@
+#include <stdio.h>
+#include <assert.h>
+#include <stdlib.h>
+
+#define SHOW(x, fmt) printf( #x ": " fmt "\n", x )
+
+#ifdef ERRS
+#define ERR(...) __VA_ARGS__
+#else
+#define ERR(...)
+#endif
+
+// int main( int argc, const char *argv[] ) {
+//     assert(argc == 2);
+//     const int n = atoi(argv[1]);
+//     assert(0 < n && n < 1000);
+
+//     float a1[42];
+//     float a2[n];
+//     SHOW(sizeof(a1), "%zd");
+//     SHOW(sizeof(a2), "%zd");
+
+// }
+
+
+    // SHOW(sizeof( a   ), "%zd");
+    // SHOW(sizeof(&a   ), "%zd");
+    // SHOW(sizeof( a[0]), "%zd");
+    // SHOW(sizeof(&a[0]), "%zd");
+
+
+
+int main() {
+
+/*
+When a programmer works with an array, C semantics provide access to a type that is different in every way from ``pointer to its first element.''
+
+Its qualities become apparent by inspecting the declaration
+*/
+    float a[10];
+/*
+
+The inspection begins by using @sizeof@ to provide definite program semantics for the intuition of an expression's type.
+
+Assuming a target platform keeps things concrete:
+*/
+    static_assert(sizeof(float)==4);    // floats (array elements) are 4 bytes
+    static_assert(sizeof(void*)==8);    // pointers are 8 bytes
+/*
+
+Consider the sizes of expressions derived from @a@, modified by adding ``pointer to'' and ``first element'' (and including unnecessary parentheses to avoid confusion about precedence).
+*/
+    static_assert(sizeof(  a    ) == 40); // array
+    static_assert(sizeof(& a    ) == 8 ); // pointer to array
+    static_assert(sizeof(  a[0] ) == 4 ); // first element
+    static_assert(sizeof(&(a[0])) == 8 ); // pointer to first element
+/*
+That @a@ takes up 40 bytes is common reasoning for C programmers.
+Set aside for a moment the claim that this first assertion is giving information about a type.
+For now, note that an array and a pointer to its first element are, sometimes, different things.
+
+The idea that there is such a thing as a pointer to an array may be surprising.
+It is not the same thing as a pointer to the first element:
+*/
+    typeof(& a    ) x;   // x is pointer to array
+    typeof(&(a[0])) y;   // y is pointer to first element
+                       ERR(
+    x = y;             // ill-typed
+    y = x;             // ill-typed
+                       )
+/*
+The first gets
+    warning: warning: assignment to `float (*)[10]' from incompatible pointer type `float *'
+and the second gets the opposite.
+*/
+
+/*
+We now refute a concern that @sizeof(a)@ is reporting on special knowledge from @a@ being an local variable,
+say that it is informing about an allocation, rather than simply a type.
+
+First, recognizing that @sizeof@ has two forms, one operating on an expression, the other on a type, we observe that the original answers are unaffected by using the type-parameterized form:
+*/
+    static_assert(sizeof(typeof(  a    )) == 40);
+    static_assert(sizeof(typeof(& a    )) == 8 );
+    static_assert(sizeof(typeof(  a[0] )) == 4 );
+    static_assert(sizeof(typeof(&(a[0]))) == 8 );
+
+/*
+Finally, the same sizing is reported when there is no allocation at all, and we launch the analysis instead from the pointer-to-array type.
+*/
+    void f( float (*pa)[10] ) {
+        static_assert(sizeof(   *pa     ) == 40); // array
+        static_assert(sizeof(    pa     ) == 8 ); // pointer to array
+        static_assert(sizeof(  (*pa)[0] ) == 4 ); // first element
+        static_assert(sizeof(&((*pa)[0])) == 8 ); // pointer to first element
+    }
+    f( & a );
+
+/*
+So, in spite of considerable programmer success enabled by an understanding that
+an array just a pointer to its first element (revisited TODO pointer decay),
+this understanding is simplistic.
+*/
+
+/*
+A shortened form for declaring local variables exists, provided that length information is given in the initializer:
+*/
+    float fs[] = {3.14, 1.707};
+    char cs[] = "hello";
+
+    static_assert( sizeof(fs) == 2 * sizeof(float) );
+    static_assert( sizeof(cs) == 6 * sizeof(char) );  // 5 letters + 1 null terminator
+
+/*
+In these declarations, the resulting types are both arrays, but their lengths are inferred.
+*/
+
+}
+
+
+void syntaxReferenceCheck(void) {
+    // $\rightarrow$ & (base element)
+    //     & @float@ 
+    //     & @float x;@ 
+    //     & @[ float ]@
+    //     & @[ float ]@
+    float x0;
+
+    // $\rightarrow$ & pointer
+    //     & @float *@ 
+    //     & @float * x;@ 
+    //     & @[ * float ]@
+    //     & @[ * float ]@
+    float * x1;
+
+    // $\rightarrow$ & array 
+    //     & @float[10]@ 
+    //     & @float x[10];@ 
+    //     & @[ [10] float ]@
+    //     & @[ array(float, 10) ]@
+    float x2[10];
+
+    typeof(float[10]) x2b;
+
+    // & array of pointers
+    //     & @(float*)[10]@
+    //     & @float *x[10];@
+    //     & @[ [10] * float ]@
+    //     & @[ array(*float, 10) ]@
+    float *x3[10];
+//    (float *)x3a[10];  NO
+
+    // $\rightarrow$ & pointer to array
+    //     & @float(*)[10]@
+    //     & @float (*x)[10];@
+    //     & @[ * [10] float ]@
+    //     & @[ * array(float, 10) ]@
+    float (*x4)[10];
+
+    // & pointer to array
+    //     & @(float*)(*)[10]@
+    //     & @float *(*x)[10];@
+    //     & @[ * [10] * float ]@
+    //     & @[ * array(*float, 10) ]@
+    float *(*x5)[10];
+    x5 =     (float*(*)[10]) x4;
+//    x5 =     (float(*)[10]) x4;  // wrong target type; meta test suggesting above cast uses correct type
+
+    // [here]
+    // const
+
+    // [later]
+    // static
+    // star as dimension
+    // under pointer decay:                int p1[const 3]  being  int const *p1
+
+    const float * y1;
+    float const * y2;
+    float * const y3;
+
+    y1 = 0;
+    y2 = 0;
+    // y3 = 0; // bad
+
+    // *y1 = 3.14; // bad
+    // *y2 = 3.14; // bad
+    *y3 = 3.14;
+
+    const float z1 = 1.414;
+    float const z2 = 1.414;
+
+    // z1 = 3.14; // bad
+    // z2 = 3.14; // bad
+
+
+}
+
+#define T float
+void stx2() { const T x[10];
+//            x[5] = 3.14; // bad
+            }
+void stx3() { T const x[10];
+//            x[5] = 3.14; // bad
+            }
Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
@@ -0,0 +1,111 @@
+#include <assert.h>
+int main() {
+
+/*
+The last section established the difference between these four types:
+*/
+
+    float    a  [10] ;          // array
+    float (*pa )[10] = & a    ; // pointer to array
+    float    a0      =   a[0] ; // element
+    float  *pa0      = &(a[0]); // pointer to element
+
+/*
+But the expression used for obtaining the pointer to the first element is pedantic.
+The root of all C programmer experience with arrays is the shortcut
+*/
+    float  *pa0x     =   a    ; // (ok)
+/*
+which reproduces @pa0@, in type and value:
+*/
+    assert( pa0 == pa0x );
+/*
+The validity of this initialization is unsettling, in the context of the facts established in the last section.
+Notably, it initializes name @pa0x@ from expression @a@, when they are not of the same type:
+*/
+    assert( sizeof(pa0x) != sizeof(a) );
+
+
+
+
+
+
+
+
+
+
+
+
+
+    void f( float x[10], float *y ) {
+        static_assert( sizeof(x) == sizeof(void*) );
+        static_assert( sizeof(y) == sizeof(void*) );
+    }
+    f(0,0);
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    // reusing local var `float a[10];`
+    float v;
+    f(  a,  a ); // ok: two decays, one into an array spelling
+    f( &v, &v ); // ok: no decays; a non-array passes to an array spelling
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    char ca[] = "hello";    // array on stack, initialized from read-only data
+    char *cp = "hello";     // pointer to read-only data [decay here]
+    void edit(char c[]) {   // param is pointer
+        c[3] = 'p';
+    }
+    edit(ca);               // ok [decay here]
+    edit(cp);               // Segmentation fault
+    edit("hello");          // Segmentation fault [decay here]
+
+
+
+
+
+
+
+
+
+
+
+
+    void decay( float x[10] ) {
+        static_assert( sizeof(x) == sizeof(void*) );
+    }
+    static_assert( sizeof(a) == 10 * sizeof(float) );
+    decay(a);
+
+    void no_decay( float (*px)[10] ) {
+        static_assert( sizeof(*px) == 10 * sizeof(float) );
+    }
+    static_assert( sizeof(*pa) == 10 * sizeof(float) );
+    no_decay(pa);
+}
Index: doc/theses/mike_brooks_MMath/programs/bkgd-carray-mdim.c
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-carray-mdim.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-carray-mdim.c	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
@@ -0,0 +1,59 @@
+#include <stdio.h>
+#include <assert.h>
+#include <stdlib.h>
+
+#define SHOW(x, fmt) printf( #x ": " fmt "\n", x )
+
+#ifdef ERRS
+#define ERR(...) __VA_ARGS__
+#else
+#define ERR(...)
+#endif
+
+
+
+int main() {
+
+/*
+As in the last section, we inspect the declaration ...
+*/
+    float a[3][10];
+/*
+
+*/
+    static_assert(sizeof(float)==4);    // floats (atomic elements) are 4 bytes
+    static_assert(sizeof(void*)==8);    // pointers are 8 bytes
+/*
+
+The significant axis of deriving expressions from @a@ is now ``itself,'' ``first element'' or ``first grand-element (meaning, first element of first element).''
+*/
+    static_assert(sizeof(  a       ) == 120); // the array, float[3][10]
+    static_assert(sizeof(  a[0]    ) == 40 ); // its first element, float[10]
+    static_assert(sizeof(  a[0][0] ) == 4  ); // its first grand element, float
+
+    static_assert(sizeof(&(a      )) == 8  ); // pointer to the array, float(*)[3][10]
+    static_assert(sizeof(&(a[0]   )) == 8  ); // pointer to its first element, float(*)[10]
+    static_assert(sizeof(&(a[0][0])) == 8  ); // pointer to its first grand-element, float*
+
+    float (*pa  )[3][10] = &(a      );
+    float (*pa0 )   [10] = &(a[0]   );
+    float  *pa00         = &(a[0][0]);
+
+    static_assert((void*)&a == (void*)&(a[0]   ));
+    static_assert((void*)&a == (void*)&(a[0][0]));
+
+    assert( (void *) pa == (void *) pa0  );
+    assert( (void *) pa == (void *) pa00 );
+
+//    float (*b[3])[10];
+    float *b[3];
+    for (int i = 0; i < 3; i ++) {
+        b[i] = malloc(sizeof(float[10]));
+    }
+    a[2][3];
+    b[2][3];
+/*
+
+*/
+
+}
Index: doc/theses/mike_brooks_MMath/programs/bkgd-cfa-arrayinteract.cfa
===================================================================
--- doc/theses/mike_brooks_MMath/programs/bkgd-cfa-arrayinteract.cfa	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
+++ doc/theses/mike_brooks_MMath/programs/bkgd-cfa-arrayinteract.cfa	(revision 4c2fe47e178e4074ffe9d1387cbe05d69e4c0db3)
@@ -0,0 +1,32 @@
+// #include <time.h>
+//#include <stdlib.hfa>
+
+struct tm { int x; };
+forall (T*) T* alloc();
+
+int main () {
+    // // // C, library
+    // // void * malloc( size_t );
+    // // C, user
+    // struct tm * el1 = (struct tm * ) malloc(      sizeof(struct tm) );
+    // struct tm * ar1 = (struct tm * ) malloc( 10 * sizeof(struct tm) );
+
+    // // // CFA, library
+    // // forall( T * ) T * alloc();
+    // // CFA, user
+    // tm * el2 = alloc();
+    // tm (*ar2)[10] = alloc();
+
+
+
+
+    // ar1[5];
+    // (*ar2)[5];
+
+
+
+    // tm (&ar3)[10] = *alloc();
+    tm (&ar3)[10];
+    &ar3 = alloc();
+    ar3[5];
+}