3.自动验证

刚才在一本关于系统验证的书里读到关于自动验证（比如在不运行一个程序的情况下验证这个程序不会进入死锁）理论的历史。书里说自动验证的鼻祖是莱布尼兹。他设想了一种语言叫lingua characteristica, 并设想了一种机器叫caculus ratiocinator，可以运行这种语言，推出各种各样的真理。让我对这个大牛佩服的地方是，他的计划横跨三个世纪！！！。这个计划激励了无数牛人前赴后继，导致了微积分的诞生，布尔代数的问世，谓词逻辑的降临。。。虽然莱老大的目标不可能实现了（因为一个叫歌德尔德老大证明了这是不可能的），但由之催生的理论却奠定了现代数学进而现代计算理论的基础。简直是古人所谓“取法乎上乃得其中”的最佳写照。

P.S. 书是讲理论的教科书，本不好读，但前面近四十页的理论演化简史（家谱）一下让看似枯燥的理论变得引人入胜，而且让理论呈现出清晰的脉络，实在体现了作者的匠心。