这周一直在看 OpenGL 的材料，没时间思考什么大块的东西（正在惶恐是不是以后会越来越多地写下这句话）。零零碎碎的有些可以记的东西。首先说个题目里没有的东西，国内访问不到的网站越来越多了。昨天居然连 arstechnica.com 都被墙了几个小时（也许是地震？）。Wordpress-china.com 回光返照了一天，还没来得及迎接我的一篇文章，就再次倒下了。
大多数时间在看《 Interactive Computer Graphics: A Top-Down Approach Using OpenGL, Fifth Edition 》。同时看 Apple 的 OpenGL Programming Guide 。前者的第一章根本没谈 OpenGL，海侃了一番计算机图形的发展，本打算略过，最后还是坚持读了。不算白费功夫，确实搞清了很多一直以来疑问。比如 LCD、LED 和等离子三种显示方式有什么不同——前者每个像素是一个液晶极化挡板，依靠遮挡背光来变换颜色，后两者每个像素都是一个独立光源，但是发光原理不同。还有为什么 GPU 比 CPU 处理图像更快，这也是 MMX 指令集的原理——多步骤流水线，同一组指令（对于软件呈现为单一条指令）处理大量数据，代价是处理分支的能力很弱或者没有。
这周在网上看到的最激动人心的新闻是 L4 微内核的安全性得到了形式证明。这些年来一直在学习如果把软件做的更优秀和健壮。虽然感受颇多，但是都是一些近乎于无形的东西。L4 的形式证明说明业界已经开始得到一些有形的突破性成果。也许明天会达到形式证明一个系统的功能性正确，或者证伪一个系统的功能性正确并且指出错误。
这周学到的最有用的知识的途径是通过一个愚蠢的错误。昨天我对甫鸼说打算在家里建一个 Git server。甫鸼当下大不解：「为什么是 server ？」没说两句我开始意识到自己一定是犯了一个愚蠢的错误。立刻打开 Wiki 的 Git 词条。果然第二段就赫然写着：『 Every Git working directory is a full-fledged repository with complete history and full revision tracking capabilities, not dependent on network access or a central server. 』
希望在自己的笔记本上建立单机的代码库已经很久了。两年多以前就在思考为什么没有人写一个不依赖 server 的 version control 系统。现在才明白，这就是分布式 version control 系统的基本功能。这个名称很早就听说了，如果自己能看一下大致的介绍，也就不会困惑许久甚至打算自己写一个。都说不了解 UNIX 的用更差的方式发明 UNIX，我也是在自己的头脑里用更差的方式发明了分布式 version control 这个概念——其实还不到那一步，只是想到了本地版本管理而已，也就是 Git 最初实现的第一步。虽然把 version control 视为人类文明发展的奠基石，居然连分布式系统的概念都不清楚。学习了 Git 也连带看了 Linus 对 CVS 一类系统的批判。今天试用了 Git ，很好用也很强大。Linus 不愧是大师。Linus 和 Steve Jobs 的共同点就是他们设计的第一个产品就改变了世界，但是他们还能继续创造第二个。
技术奇异点 
2009/08/22 1:47 上午 |
有杂记就有杂评：
墙的问题不做大片评论了，很有趣的是我从美国访问国内的网站完全感觉不到有网速变慢的现象。不知是错觉，还是自己的忍耐能力提高？
东哥涉猎广泛：OpenGL这东西我想了好几年，最终还是没开始看。
L4 的形式证明：最近孤陋寡闻了，没有注意这个消息。不过从官方连接的论文来看（http://ertos.nicta.com.au/research/sel4/）似乎语焉不详，没有明确指出证明的对象是算法还是代码。如果说是证明了算法，那么只能说我们还在原地踏步：一直以来计算机世界里首要面对的问题都是编程错误而不是算法错误。这就是过去十年形式证明逐步被模型检查和软件测试这两个方向超越的原因。恐怕现在也只有那些真正的“计算机科学家”（我的意思是：常年坐在某个研究所的办公室里，从未写过软件给*别人*用的计算机专家们）才会相信证明算法正确等于软件正确。
不过无论如何，有文章总是好的。周末俺慢慢研究，回头再做正式的评论。
关于Git：考虑到数据安全和发布的需要，即使git也还是需要一个server的，对国外来说GitHub（http://github.com/）是个不错的选择。在本地移动硬盘保存也无妨，但对于发布来说也简陋了些。
顺便说一句，git功能强大，不过对Windows的支持现在还是差了些，这也就是我比较倾向于Mercurial(Hg)的原因。而且主要基于Python实现的Mercurial还有一些好处：跨平台，结构简单便于学习，不需要垃圾收集（git 需要不时地repack来回收磁盘垃圾）。Mercurial最大的毛病是它的branch功能弱得惊人：创建后不能删除，发布时不能选择发布单个branch。就这一点上来看，它跟git相比只能算个半成品。好在我现在对branch的需求还不强烈，而对code hosting的要求很高，毕竟google code直接支持Mercurial，而我用了很多google的服务。另外Mercuial的Roadmap里也有关于加强branch的计划，所以就先用着吧。
2009/08/27 12:30 下午 |
你如果不大发议论指点IT江山，我就会觉得写的更好些。而且我还会从你的博客学到些东西。我比较喜欢形而下的。
形式化的证明或检查首先需要形式化的输入，但对普通程序来说这太困难了，或者工作量太大。2007年的图领奖颁给了研究模型检验（Model checking）的学者，NASA好象对某些程序使用模型检验。
To fuzhou：计算机科学家应该不会傻到相信证明算法正确等于软件正确。Wirth早就说了，程序=算法+数据结构，我想能当计算机科学家的，应该会理解，而不是把这当作通俗的口号。当没能力研究两个相关事物时，先假定一个是不变的或可忽略的，这是正当的办法。
2009/08/30 12:30 下午 |
说到模型检查，巧了，我一个老友正好是在这个方向做了五年之久的。
过去几年我和他吵架给我的印象是，模型检查和程序验证仍然是两个思路，模型检查对程序形式化的要求相对要低得多，只要能描述成状态图即可，不像很多程序验证需要把程序转化成谓词。即便如此，由于难以找到通用的方法避免状态爆炸，现在模型检查的能力仍然是有限的，难以大规模应用——我确实肯定的成功案例是阎良试飞中心的无人机控制软件，他们用我们隔壁实验室做的工具检查出了三个严重bug。我也听说过NASA这几年在所有程序安全研究（程序验证，模型检查和自动测试）投入了无数的资金，不过我们实验室没有和他们合作过，也就不知详情。
我大概过了一遍L4主页上连接的其中一篇论文，从内容来看他们走的还是程序验证的思路。所以我的第一感觉是这不对路，加上论文中他们也有很多地方没有解释清楚，比如如何用他们自己写的工具将bitfield映射成page table entries，以及这如何影响程序证明。或许我这几年没怎么关心过程序验证的进展所以没有看懂，如果志岩兄有什么最新消息，还望赐教。
2009/08/30 11:58 上午 |
嘿嘿，如果他们真的有这么明智的话可麻烦了，那我就没法解释形式证明前十年的热火究竟从何而来。
=== 以下是个人的牢骚，不针对个人，冒犯之处万望见谅 ===
我一直认为“计算机科学家”是个伪概念，这只是一些掌握了话语权又不做实事的理论数学家们自封的头衔而已。在我看来，研究算法也好，数据结构也罢，我只能承认他们是数学家，他们和我们的关系类似于力学和建筑学，有交集但截然不同。所以我总是很严肃地对待诸如时间复杂度和LALR(1)算法的话题，但是想让我承认他们“证明”了某个软件是安全的，恕难从命。