Re: Why would anyone want opacity?

[Matthias Blume <blume@CS.Princeton.EDU>]

From: "Guillermo J. Rozas" <gjr@martigny.ai.mit.edu>
Subject: Re: Why would anyone want opacity?
Date: Thu, 9 May 96 16:40:51 -0400

> Thus type checking _should be_ a property of tools, not languages,
> since languages make perfect sense in the absence of _any_ mechanized
> tools.

No, they don't.  It doesn't matter if the `mechanized' checker has
been implemented.  It is only important that it can be done.  For the
purpose of CS every language definition induces the description of a
mechanical checker.

To be able to do type-checking by hand on a blackboard you need an
algorithm for doing so.  Once you have the algorithm, you might as
well implement it on a computer.  Once you have it on a computer, you
might as well use it, because type-checking is often very tedious.
The computer will not make those small mistakes that are almost
unavoidable in a hand-performed ten-page derivation.

In order to be able to do any type-checking at all (be it because the
language definition tells you to, or be it because you use an add-on
tool) you need to follow typing rules.  Those rules are inevitably
married very closely to syntax and semantics of the language itself.
So you might as well describe the typing rules together with the rest
of the language.

We all know that types aren't strictly *necessary*.  After all, there
is Scheme, and there are Smalltalk, C, Assembly, ...  It all comes down
to whether we find strong typing *useful*.  For a long time I was with
you and didn't find it terribly useful -- because I never put it to
good use.  Once I discovered the benefits I didn't want to do without
them anymore, even though I know I could if I had to.

-Matthias