Re: Types Considered Harmful

Victor Yodaiken (yodaiken@sphinx.nmt.edu)
Mon, 8 Aug 1994 10:13:38 -0600

On Aug 8, 8:39am, Robert S. Boyer wrote:
Subject:
>Manifestly, to anyone who has studied set theory as a foundation for
>mathematics, there was no new science in Lamport's piece. Nor was
>there intended to be. That was an article about the politics of
>science. Is your point that every article in computer science ought
>only to be written for people with a good grasp of the foundations of
>mathematics?

No. I'm just at a loss to see what point was being made other than
"everything can be encoded in sets". If that is the only point, then
it could have been made more simply.

>I think Lamport's piece was and is a good and worthy article. Where
>else do you find a statement of the position, by a computer scientist,
>for computer scientists, that all this type stuff that so dominates so
>much of computer science theory and formal design, is a probably
>largely a waste of time? If you do know of other such articles, I

I believe that there is an extensive literature on this subject in
the field of programming language design. One of the most
interesting couple of paragraphs on this subject can be found in the
Mathematica book by Wolfram.

>I think a discussion of types is especially relevant to the QED
>business. It seems to me that one of the many reasons that QED-like
>projects don't catch on more is that the world is so divided between
>those who love types (both those from a programming language
>background and also the followers of de Bruijn and Martin-Lof) and
>those who have no use for types (largely those with an upbringing in
>set theory as a foundation for mathematics). For people like de

Or Skolem style recursive arithmetic: as you well know, one can
encode sets into integers perhaps more simply than the reverse.