From owner-qed Mon Aug 8 13:45:38 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA18433 for qed-out; Mon, 8 Aug 1994 13:44:45 -0500 Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id NAA18423 for ; Mon, 8 Aug 1994 13:44:37 -0500 Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id MAA07462; Mon, 8 Aug 1994 12:47:20 -0600 Message-Id: <199408081847.MAA07462@chelm.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Mon, 8 Aug 1994 12:47:19 -0600 In-Reply-To: "Phil Windley" "Re: Types Considered Harmful" (Aug 8, 9:55am) reply_to: yodaiken@chelm.nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: "Phil Windley" , John Harrison Subject: Re: Types Considered Harmful Cc: qed@mcs.anl.gov (qed list), info-lal@leopard.cs.byu.edu Sender: owner-qed@mcs.anl.gov Precedence: bulk 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?