Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!ucbvax!hplabs!hpfcso!mjs
From: mjs@hpfcso.HP.COM (Marc Sabatella)
Newsgroups: comp.lang.misc
Subject: Goedel & programming languages
Message-ID: <8960009@hpfcso.HP.COM>
Date: 31 Jan 90 15:54:13 GMT
Organization: Hewlett-Packard, Fort Collins, CO, USA
Lines: 24

An off the wall question:

Everyone knows the basic diagonalization argument showing that there are some
number-theoretic functions which are not computable.  But after reading
Hofstadter's pop-philosophy classic, "Goedel, Escher, Bach", in which the
author makes several (rather lame) analogies from Goedel's Incompeteness
theorem to, among other things, DNA and record players, I wonder if there is
not a more powerful statement to be made.

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)
Disclaimers:
	2 + 2 = 3, for suitably small values of 2
	Bill and Dave may not always agree with me