From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,86fd56abf3579c34
X-Google-Attributes: gid103376,public
X-Google-Thread: 10db24,77f71d0bde4c5bb4
X-Google-Attributes: gid10db24,public
From: dewar@cs.nyu.edu (Robert Dewar)
Subject: Re: What good is halting prob?
Date: 1995/04/19
Message-ID: <dewar.798271681@gnat>#1/1
X-Deja-AN: 101283225
references: <3kaksj$iur@isnews.calpoly.edu> <cppD77Ex6.E77@netcom.com>
 <3mve9b$gaj@news.cais.com> <cppD7880n.32B@netcom.com>
 <3n285v$9vl@news.cais.com>
organization: Courant Institute of Mathematical Sciences
newsgroups: comp.lang.ada,comp.edu
Date: 1995-04-19T00:00:00+00:00
List-Id: <comp.lang.ada>

Randy says:

"And correctness is not subjective.  It simply means that the program will
always behave as expected, regardless of the input.  If by correctness,
you are thinking of "not incorrect", or "acceptably correct ..."

I think that's potentially misleading. Correctness has to do with conformance
to a formal specification, at least the way the term is used when you talk
about "proof of correctness".

Suppose you expect a compiler to always give clear understandable error
messages. That's a reasonable expectation, but you can't formalize it.
So correctness could not capture this informal expectation.

On the other hand, given a formal definition of the language you are compiling,
it is at least conceptually feasible to prove that a compiler gives an error
message of *some* kind for any incorrect program.