That might have been the message, but the title was "Types Considered
Harmful".
| But the paper was quite a good read, and the topic merits discussion. I'm
| an agnostic on the question, though I am much more familiar with formal
| proofs in type theory than set theory. It may only be when we push
| formalization into more complicated parts of mathematics that we have the
| perspective to decide the issue.
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.
Of course, this argument hinges on the assumption is that the harm is
greater than the benefit, so Lamport states: "Our experience has been that,
when writing a rigorous proof of a theorem, one quickly finds any error in
its statement that could be caught by a type checker." I don't doubt this
is true for Lamport or the majority of readers of this list. However, my
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.
One could argue that that these were students in unfamiliar territory and
they would have eventually gotten the hang of doing the syntax and type
checking themselves. Also, real engineers using a specification language
wouldn't be so quick to accept anything so long as it looked complicated.
These arguments are probably true, but even so, most of the people who
would write formal specifications are never going to be mathematicians of
Lamport's stature. The essence of engineering is developing methodologies
that allow even mediocre people to do acceptable work. If we are to get
past the stage were specification and verification are the domain of
virtuosos, we will have to provide methods and tools that aid writing
specifications.
I would argue, therefore, that for the majority of people, the harm done by
the type system is minor compared to the benefit that the type system
provides. I don't believe that Lamport has made a convincing argument on
this point and without it, his conclusion seems flawed. To observe that
brilliant mathematicians are often better off without types and then
conclude that specification languages are therefore better off without them
is an argument that I can't buy.
--phil--
__________________________________________________________________________
Phillip J. Windley, Asst. Professor | windley@cs.byu.edu
Laboratory for Applied Logic |
Dept. of Computer Science, TMCB 3370 |
Brigham Young University | Phone: 801.378.3722
Provo UT 84602-6576 | Fax: 801.378.7775
------------------------------------------------------------------------
If you use WWW, I'm <A HREF="http://lal.cs.byu.edu/people/windley/windley.html">here</A>.