面向计算机科学的数理逻辑系统建模与推理《无可奈何的Delay》

某日在CU上与人瞎掰，其间谈到SICP序言太过深奥，于是有人抱怨道：我从来不看序，都是些吹捧之辞，毫无价值云云。要放到平时，我会十分赞同这个观点，如果你觉得有失偏颇，那在豆瓣上随便搜一堆书找出序言来看看是否大部分异曲同工、马屁之声不绝于耳。可问题这次谈及SICP，我便有些隐隐心痛————这可是Perlis写的序，再说，也没有大师给小弟拍马的道理。Perlis在这篇序言中引用了很多当年他自己的名篇《编程警言》的句子，看上去似乎数学味道很浓很艰深，实则为一篇充满诙谐幽默的随笔。要不怎么说人家是大师，光知道嘣俩牛B词汇出来吓唬人怎么行。回想某些国内大师的著作，翻开我就晕了，几乎是全面颠覆我以前的理解，每每及此，我便感慨：这世界真是变化快，咱国内的计算机水平都超越老外了，都全面颠覆计算理论了。然后不由得为自己的不学无术和落后感到脸红，估摸这自己这水水，还是继续看SICP之类的幼儿教科书比较实在，国内大师之巨著就暂时不敢奢望了。

这本LCS吸引我的同样是序言，当然由于我了解信息的局限性，直到08年我才真正认识到这篇序言的价值，因为序言的作者E.Clark在08年因Model Checking而获图灵奖。而本书，恰是Model Checking的理论基础。再看译本出版时间为07年7月，我便深刻感受到本书译者对于计算科学发展方向的敏感性。要知道本书出版近8个月后，Model Checking才由于图灵奖而被众人熟知。所以本书绝不是什么应景之作，反而可说是极具洞察的一本书。

不过么～Clark相比Perlis来，或许在学术上青出于蓝，要说整体素质，离伯大师还差得远。光对比序言水平就能看出来，Perlis可说是综合数学、艺术、文学的大师，而Clark就是一典型的科学家。恩～这样的一种对比当然从实际意义上来说毫无价值，纯粹是个人感情抒发，对本书有兴趣的人千万不要被这个对比打击到热情。

本书另一处令人惊奇的地方，是二位作者来自于英国学校，这或许让不少关注计算科学书籍的人感到略微意外，毕竟在很多人心目中，MIT博克利斯坦福CM等等美国院校才应该与牛书挂钩才是。哎～要是图灵在天得知世人皆如此仰视米国而忽视其祖国，不知其做何感受。

对于本书的价值，应该说懂得的人不需要听解释，不懂的人估计解释了也没用。或许可以用这么一个简单的例子来说明本书价值：可能有的朋友立志于开发中国的Quartus、ModelSim什么的，那你们有福了，本书可以带你们跨入理论门槛。当然你可能会有这样的担心，Qartus之流都基于特定的平台，即便我们研究了，能写软件了，以中国目前的硬件发展水平，怕也是望梅止渴。你能这么想，是很好的，至少说明你不是埋头撞墙的书呆子。不过正像我前面说的，这个世界发展太快了，现在OpenSparc这么火爆，我个人认为，有志向的人还是不要担忧自己很牛B了，周围却没有牛B的人来响应，而更应该担心别人牛B起来了，自己却没本事响应别人。如果你觉得自己很牛B了，但身边的人很磋，那说明你不够牛B。一个真正牛B的人，不可能身边围绕着一群磋人。

恩～在这里还是要悄悄说一句，本书的价值可不仅仅在于能开发个Quartus之类除了能赚钱外一无是处的东东，更为关键的价值在于系统验证。这才是一统天下的不二法宝，因为你的验证水平很高的情况下，就可以制定标准，有了标准等同于列土封王。当然，这是学术上的了，不大适合个人发展，我觉得对于普通人来说能写个Quartus当个首富什么的也就算功成名就了。

就本书内容而言，主要就是两部分，前两章讲归约，后面的讲验证。本质上来说，归约是为了简化问题以方便验证，验证是为了保证系统能如预定般工作。整套形式化验证理论不外乎就是这么简单一句话，不过越简单的描述才越发令人毛骨悚然。总之，在这么一个简单描述的背后，隐含的是非常艰难的研究工作。本书我只打4颗星，对于大部分人来说，知道这本书的背景和大体内容，就算不错了。真正愿意研究下去的人，恐怕也不屑于此书。