Changeset 6a8c773

Timestamp:

Mar 24, 2024, 11:08:46 PM (9 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

41fb996

Parents:

82e5670

Message:

more work on introduction

File:

• doc/theses/mike_brooks_MMath/intro.tex (modified) (2 diffs)

doc/theses/mike_brooks_MMath/intro.tex

@@ -33 +33 @@
 
 
-\section{C/\CFA}
+\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 the C.
+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.
+Hence, it is assumed the reader has a medium knowledge of C or \CC, on which extensive new C knowledge is built.
 
 
-\subsection{Common knowledge}
+\subsection{C?}
 
-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
+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.
+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.
+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 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
+        \item the compiler accepts or rejects certain syntax,
+        \item the prints output to buttress a claim of behaviour,
+        \item executes without triggering any embedded assertions testing pre/post-assertions or invariants.
 \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.
+This work has been tested across @gcc@ versions 8--12 and clang version 10 running on ARM, AMD, and Intel architectures.
+Any discovered anomalies among compilers or versions is discussed.
 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}
+\subsection{Ill-Typed Expressions}
 
-These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
+C reports many ill-typed expressions as warnings.
+For example, these attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
 \lstinput{12-15}{bkgd-c-tyerr.c}
 with warnings:
@@ -86 +76 @@
 \end{cfa}
 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.
+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.
 
-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.
+% 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
+% 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.
+% *1  TAPL-pg1 definition of a type system