misleading article on type checking procedure parameters

[ms1g@ANDREW.CMU.EDU (Mark Steven Sherman)]

I felt very uneasy about the claim that procedure parameters/variables cannot
be typed checked at compile time, since 1) I had written a compiler that purported
to do that and 2) there is a widely publicized result by Ed Clarke to the effect
that if one has *all* of procedure parameters, global variables, static scope,
recursion and something else (I think reference parameters), then one cannot
create a sound, complete axiomatic description of the language (in the sense
of Cook) but if you drop one of those requirements, then you can. Naturally,
the referenced Acta Informatica article implied that 4 of Clarke's conditions
were superflous -- if you can't type check it, you can't prove it. So I looked
up the article. It says something much, much weaker, and uses 30 pages of formalisms
to demonstrate, to my mind, the obvious. The property of Algo-60 (and purported
property of PL/1) that makes it impossible to type check is that procedure parameters
(there are no procedure variables in Algol-60) do not have their formal parameters
specified anywhere -- with the trivial exception of return types, you merely
say that an identifier denotes a procedure -- of course one can't guarantee
type correctness. I submit the following pseudo-Algol-60 demonstration program
which I hope Acta Informatica will publish as soon as they can: 

begin

   comment "formality" ; 

   boolean procedure CheckHalt(TuringIndex);@*
       integer TurindIndex@*
   begin@*
     comment Insert your favorite turing machine simulator ;@*
     if halts return true else return false;@*
   end;

   comment procedure that will fail as necessary; 

   procedure test(q);@*
      procedure q;@*
   begin@*
        q(1)@*
   end;

   comment Two different possible parameters; 

   procedure p1; begin write("Lose") end; 

   procedure p2(i); integer i; begin write("Win",i) end; 

   comment Value to read; 

   integer WhichMacine; 

   read(WhichMachine);@*
   if CheckHalt(WhichMachine) then test(p1) else test(p2)

end

I'll even change the input to a constant -- you give a compiler that can tell
me if this program generates a runtime (type check) error, and I'll solve the
halting problem.

By the way, the PL/1 compiler I have been using for the last three years does
indeed require that I specify parameter and return types for all entries, including
nested entries, which meets the requirements of the article. Note: there is
no need to distinguish name equivalence and structural equivalence. The article
only talks about completely specifying the parameters or not. (By the way, the
reason the artcile is so long is that it actually considers four classes of
languages: 1) nothing about procedures' signatures needs to be specified, 2)
only the return type needs to be specified, 3) return types and parameters need
to be specified, but not nested procedure parameters, i.e., the procedure parameter
must list its arguments, but if one of those arguments is also a procedure parameter,
then the most nested parameter need not be specified, and 4) everything specified.
I'll bet you're not surprised that the results are pretty much the same for
languages 1-3.)