Re: Types Considered Harmful

Victor Yodaiken (
Mon, 8 Aug 1994 12:47:19 -0600

On Aug 8, 9:55am, "Phil Windley" wrote:
Subject: Re: Types Considered Harmful
>Section 3 seems to be the heart of the paper. Everything before it is more
>or less an reminder of some things about ZF. Section 3 makes a quick
>distinction between type correctness and type checkable, stating that "Type
>correctness is a reasonable requirement for a formula. However, type
>systems generally require a formula to be type checkable..."
>Lamport's issue seems to be with the restrictions placed on type systems in
>order to make them type checkable (if I've missed something, then I'm
>afraid its all too subtle for me). He asserts that since any decidable
>type system disallows some type-correct formulas, they stand in the way of
>doing mathematics.

I've never been able to follow arguments of this form. Why is it
interesting that in the general case type checking is not decidable?
Why is decidability an interesting issue here at all? I can understand
feasability being considered important, but what's the difference for
computer science between something that cannot be computed and
something that cannot, in practice, be computed? I keep seeing
computer science papers where something is cast in terms of, say,
Pressburger arithmetic as if this provided an advantage of some sort.
Is there one?

>experience is that most of the students I introduce to FM do better if they
>have syntax and type checking available. I have taught courses using Z
>with and without mechanical aids. Without the checker, students were
>willing to hand in anything so long as it was filled with lots of neat
>symbols. With the checker, they went over their specifications enough that
>what they turned in was pretty good.

On what set of problems does Lamport base his claim?