大概是因为安全的事情, 公司安全一下子搞得特别认真.

那天看到一篇亚马逊使用TLA来做形式化验证的文章, 对TLA感兴趣了, 就找到这本入门的书看了一下. 这本书纯粹是一个DSL语言和工具的使用, 实际上并没有牵涉到太多的数学的东西. 只要能看懂函数式语言, 基本上都能够看懂. 但是担心不用就会忘了, 所以当笔记一样把比较重要的东西给翻译了一下.

但是, 这个东西其实还是只适用于算法的验证, 而不是什么业务流程的实现和代码的验证.

后来我们联系了华东师大的一位做形式化设计的著名教授来交流过一次，他参与过上海地铁的软件设计。那个是真的需要形式化来证明软件的正确性。但是了解下来感觉，即使是华为，像我们这种需要7x24x356连续工作的RRU设备，用形式化也太奢侈了。即使是RRU这种相对规模比较小的产品，也超过了80万行代码，根本不可能搞什么形式化。至于人员能力水平就更不要提了，或许只有计算机科学科班出身的才知道这个是什么，像我们这种半路出家的都需要重新学习。

这个东西也就是在华为这种公司有意义，离开了之后，一般的企业根本达不到这个级别。就是屠龙技了。