🚀 go-pugleaf

In article  <1990Aug3.144312.3157@ux1.cso.uiuc.edu> morrison@thucydides.cs.uiuc.edu writes:
>
>Hello,
>
>The question has been raised on why type checking is always
>done at compile time (even conceptually).  I believe this 
>question deserves a simple answer (and it is NOT because of
>efficiency).
>
>A type system is basically a very simple and specialized 
>type of program verifyer.

This is a common misconception among people from the Pascal/Ada world.
It is true that a type system _can_ be used as a program verifier.
And this observation is arguably one of the benefits that came out of
early research in that programming language tradition.  But this is
not the only use of types.  It is also the case that a compile time
system allows for more efficient programs, and this was the original
motivation for them.  (Although, coming from assembly language, the
first langauge designers may never have considered an alternative).

However, type systems are used in mathematics where neither motivation
applies, so it seems that if there is a _true_ purpose for types, it
is the purpose used by mathematicians.  The purpose of types is simply
to group values with similar characteristics so that their behavior
may be easily described, and so that signatures may be given for
operations.  These motivations also clearly apply to programming.

>Thus a type system is simply the first modest step in program
>verification (that is determining run time behavior by analysing
>the program text).   

Of course, this is only useful if your program happens to fall into
that class of programs that has a strict enough type structure that it
is useful to to compile-time analysis.  For many programs this is not
true.
-- 
					David Gudeman
Department of Computer Science
The University of Arizona        gudeman@cs.arizona.edu
Tucson, AZ 85721                 noao!arizona!gudeman