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=-0.8 required=5.0 tests=BAYES_00,INVALID_DATE
	autolearn=no autolearn_force=no version=3.4.4
Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!linus!philabs!cmcl2!seismo!caip!sri-spam!nike!cad!ucbvax!vrdxhq.UUCP!drm1
From: drm1@vrdxhq.UUCP (Donn Milton)
Newsgroups: net.lang.ada
Subject: Re:  misleading article on type checking procedure parameters
Message-ID: <8606100004.AA26151@vrdxhq.uucp>
Date: Mon, 9-Jun-86 20:04:48 EDT
Article-I.D.: vrdxhq.8606100004.AA26151
Posted: Mon Jun  9 20:04:48 1986
Date-Received: Thu, 12-Jun-86 01:20:12 EDT
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The ARPA Internet
List-Id: <comp.lang.ada>

The key point is that parameters need to be fully specified, to
to an arbitrary (and not necessarily finite) degree of nesting, in
order to permit full type-checking.  This requires some sort of
recursive type definition for procedures.

Sherman claims that he has written a compiler that performs full type-checking,
presumably in the absence of fully specified procedure parameters.
I would be very interested in hearing more about such a compiler,
since so far Langmaack has convinced me it is impossible.

I do not have the reference to Clarke's result, but from the description
it is does not conflict with Langmaack, as long as
Clarke was referring to "fully-specified procedure parameters."
	
I also do not understand the point of the program that Sherman
presented, for which he states "you give a compiler that can tell
me if this program generates a runtime (type check) error, and I'll solve the
halting problem."  The crux of strong type-checking is that it
is done at compile-time and not at run-time.  The program should generate
a compile-time error -- it is irrelevant whether the particular portion
of the program that contains the error would be executed at run-time.
	
Donn Milton