赵翔鹏的Blog Xiangpeng's Thinkpad

由无数细节组成的系统

计算机科学总是讲abstraction。这是源自数学的思维。formal methods可以说把这个发挥到了极致。但实际系统并不是这样。不要说构建Windows这样的庞然大物，就只是要写一个实用的小软件，就会遇到无数的细节。performance，security，scalability，debugging……除了functionality之外，有无数的事情要考虑。

传统的formal methods注重functionality也没错，因为在某些情形下（比如算法领域）functionality的正确性已经够难了。但这却不是软件工程中的主要问题。

我们能做的，就是尽量挣扎着把细节包装起来。比如，工程师做出一个个框架，分出若干个层次。框架可以帮助我们，但框架并不能解决一切问题，因为好的程序员必须了解各种细节。最近读一个基于ATL/WTL的真正的product code，发现这一年来看的n本书都没白看。比如，不懂C++内存布局，不懂各种calling convention，compiler的差异，就不能理解COM的设计（btw，强烈推荐《COM本质论》的第一章）。

researcher也自有办法。因为很多细节是正交的。在TASE'09上听到Zhong Shao做的invited talk，分不同的aspect去验证汇编代码的不同性质，这个是正确的思路，而且我觉得可以做更多的东西出来。以前做business process的security验证，这个也可以归到这个思路，不过high level的东西比较虚，做起来虽然不难但并不容易很深入。而Shao对汇编和机器本身建模，比如对interrupt handling建模，这个就很有新意，且竞争者较少——很多数学系出身做formal methods的人，都不太懂系统底层。

是的，跟C++和汇编相比，写Java很容易。不过事情一旦很容易，于工业上看，就不值钱了；于学术上看，就没啥好研究的了。所以，重视各种细节吧。