🚀 go-pugleaf

In article <8960009@hpfcso.HP.COM> mjs@hpfcso.HP.COM (Marc Sabatella) writes:
>To wit, taking "formal system" to be programming language, and "proof" to be
>the parse tree and other semantic gizmos which purport that a program is valid
>in a particular language (in essence a compilation), then what do you think of
>the following statement:
>	For any programming language which is "sufficiently powerful" (meaning
>	powerful enough to write a compiler for itself?), and any compiler for
>	that language, there exists a valid program in the language which
>	cannot be compiled.
>Marc Sabatella (marc%hpfcrt@hplabs.hp.com)

Marc's statement proposed application of Godel's Incompleteness is incorrect.

The key to Godel's Incompleteness is not that a program can't be detected
to be syntactically incorrect, but rather that NO MACHINE CAN (in general)
DECIDE ANYTHING ABOUT WHAT A PROGRAM *DOES*.

It is apparent that compilers exist, and that they CAN BE both correct and
complete.  But all they can (in general) detect is syntactic correctness of
the program; they can (in general) have *no* complete knowledge about what a
program *does*.

Example: in the comp.lang.c flame war a year ago regarding the need for
"volatile" in ANSI-C, some thought a compiler could detect if a program used
a var in a "volitale" way.  But this is (again, in general) impossible.

Back to what you *can't* do: if you claim to have written a program in *any*
language that detects *anything* about what another program *does*, you'll
be incorrect -- there will always exist programs which your program will
fail on.  (naturally, if the target language is simplistic enough that it
can't do arithmetic, you *can* succeed, but most of us wouldn't call that a
"language").

Marshall Cline
--
===============================================================================
Marshall Cline/ECE Department/Clarkson University/Potsdam NY 13676/315-268-3868
 cline@sun.soe.clarkson.edu, bitnet: BH0W@CLUTX, uunet!clutx.clarkson.edu!bh0w
  Career search in progress: ECE faculty. Research oriented. Will send vitae.
===============================================================================