Changeset 43d9679 for doc/theses/mike_brooks_MMath/background.tex

Timestamp:

Aug 11, 2024, 5:33:57 PM (3 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

0e6aba06, 206ecae

Parents:

774c97e

Message:

move section from into to background

File:

• doc/theses/mike_brooks_MMath/background.tex (modified) (1 diff)

doc/theses/mike_brooks_MMath/background.tex

@@ -2 +2 @@
 
 Since this work builds on C, it is necessary to explain the C mechanisms and their shortcomings for array, linked list, and string.
+
+
+\section{Ill-typed expressions}
+
+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:
+\begin{cfa}
+warning: assignment to 'float *' from incompatible pointer type 'void (*)(void)'
+warning: assignment to 'void (*)(void)' from incompatible pointer type 'float *'
+\end{cfa}
+Similarly,
+\lstinput{17-19}{bkgd-c-tyerr.c}
+with warning:
+\begin{cfa}
+warning: passing argument 1 of 'f' from incompatible pointer type
+note: expected 'void (*)(void)' but argument is of type 'float *'
+\end{cfa}
+with a segmentation fault at runtime.
+Clearly, @gcc@ understands these ill-typed case, and yet allows the program to compile, which seems inappropriate.
+Compiling with flag @-Werror@, which turns warnings into errors, is often too strong, because some warnings are just warnings, \eg unused variable.
+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.
+
+% 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