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?