看到下面这篇文章，大名鼎鼎的Leslie Lamport写的。Lamport现在微软做并行分布式系统方面的理论研究。据说是一愤老头。还有传言说他因为太傲，拿不了图灵奖。
Should Your Specification Language Be Typed? (with Larry Paulson)
ACM Transactions on Programming Languages and Systems 21, 3 (May 1999) 502-526. Also appeared as SRC Research Report 147.
下面一段话更有趣，哈哈
In 1995, I wrote a diatribe titled
Types Considered Harmful. It argued that, although types are good for programming languages, they are a bad way to formalize mathematics. This implies that they are bad for specification and verification, which should be mathematics rather than programming. My note apparently provoked some discussion, mostly disagreeing with it. I thought it might be fun to promote a wider discussion by publishing it, and
TOPLAS was, for me, the obvious place. Andrew Appel, the editor-in-chief at the time, was favorably disposed to the idea, so I submitted it. Some of my arguments were not terribly sound, since I know almost nothing about type theory. The referees were suitably harsh, but Appel felt it would still be a good idea to publish a revised version along with rebuttals. I suggested that it would be better if I and the referees cooperated on a single balanced article presenting both sides of the issue. The two referees agreed to shed their anonymity and participate. Larry Paulson was one of the referees. It soon became apparent that Paulson and I could not work with the other referee, who was rabidly pro-types. (At one point, he likened his situation to someone being asked by a neo-Nazi to put his name on a "balanced" paper on racism.) So, Paulson and I wrote the paper by ourselves. We expected that the other referee would write a rebuttal, but he apparently never did.
