[plt-scheme] The perfect teaching language--Is this too much to ask for?

On Mon, 2009-06-15 at 13:10 -0400, Stephen Bloch wrote:
   . . .
> I'll have to think about this: "type" as a type still seems so  
> elegant, so expressively efficient :-)  My naive first impulse is to  
> suggest a consistent but incomplete static type-checker that never  
> misclassifies something's type, correctly classifies the types of  
> MOST expressions in practice, and when it can't, knows when to give  
> up so it at least terminates.  Has somebody already proven that  
> that's unattainable too?

Just a shot in the dark here:  This seems to be similar to the question
of the existence of decision procedures for classical predicate calculi.
IIRC Goedel showed that first-order PC had no decision procedure but
Herbrand showed there was a semi-decision procedure -- one that always
halted on theorems but that might spin attempting to find a
counter-example to a non-theorem (the non-theorem may have no finite
counter-examples but have an infinite one).  As I understand it
second-order PC, however, does not have even a semi-decision procedure,
for if it did it could be used to build a decision procedure for FOPC.

If something analogous holds for intuitionistic PC (the logic involved
in the Curry-Howard Correspondence) then might it defeat your incomplete
type-checker?

-- 
Bill Wood