作者／Atticbee
在这一集，Greg和RChain的研究人员Isaac，Christian讨论了TLA（Temporal Logic of Actions）和RChain的LADL（Logic As Distribution Law）。下面是Atticbee做的摘要，然后加了一些自己的理解。
TLA （Temporal Logic of Actions，行为时序逻辑）是并发系统进行形式化验证的首选工具，很多分布式的并发系统都用选用这个工具来进行验。很有意思，亚马逊的云服务就利用TLA找出了很多设计上的bug。
用TLA进行验证相对与传统的软件测试来说已经是很大的进步了。传统的测试，对于并发系统来说是远远不够的。有过多线程代码经验的码工应该有体会，有些错误是很难重现的，可能运行100万次会崩溃一次。对于非重要应用这个无所谓，因为学习这些形式化验证工具的成本很高，然后业界觉得对大多数的传统应用，有bug也无所谓，大不了重启，回滚交易。
Atticbee注：但对于区块链这种直接和钱打交道的，没法回滚的去中心化系统，这种bug就很要命了。尽管有些项目用了更安全的语言比如Rust，以及更安全的设计模式如OCAP来减少很多bug，但是智能合约的安全性是0和1的关系，不是0.9999999和1的关系。只要不通过形式验证，黑客总是可以用模型检测器找到发起攻击的途径。
用TLA进行验证，有个重要的缺陷就是，TLA的模型语言和最后的产品实现语言是不同的。在TLA的流程中，你首先用TLA建模语言定义一个模型，然后用这个语言定义一些目标性质（比如没有死锁，系统不会进入非法状态等等），最后用这个自动化工具检验这个模型是否满足指定的目标性质。检验完成后，产品代码按照这个模型来实现。然而，你验证了TLA模型的正确性，并不表明你最后的代码实现是正确的。
Atticbee注：这就好比你设计了一座桥，进行力学计算验证了这座桥是安全的，但你最后的工程实施如果和设计有所差距，造出的桥还是会倒。
所以，最好的解决方案就是，发明一种语言，它既可以是用来形式验证的建模语言，同时又可以作为产品化的代码语言。这就是为什么我们对名字空间逻辑中的LADL感兴趣的原因。Rholang中的名字空间逻辑可以用来建立一套行为类型系统，对很多有意思的性质进行表达和检查。所以在这个意义上，Rholang同时是一个产品化的代码语言，也是一个TLA那样的形式化建模语言。
Rholang可以推导出的类型可以表达TLA能验证的同样的目标性质，实际上更接近空间逻辑模型检测器（Spatial Logic Model Checker）能验证的目标性质。但Rholang的名字空间逻辑更具有表达力，因为由于反射它可以检查名字之间的结构。所以有很多事，Rholang的名字空间逻辑可以做，但Spatial Logic Model Checker做不到。一个很好的例子就是编译期的防火墙：在类型检查期间（远在代码执行之前），你就可以判断一个进程是否只在规定的名字集合中进行通信，而不会超出这个范围。甚至，你可以随时调整这个约束，比如规定在某些状态下你的进程可以在规定的名字上进行通信。这种都是在代码类型检查期间完成的，所以称之为编译期防火墙。
注意现有的RChain还没有实现这个名字空间逻辑，这是金星的规划，水星是不带类型的。尽管在Rholang 0.1的规格中，Greg给出了一个类型系统的草案，但还有很多事情要做，比如让类型定义的语法变得对开发人员更加友好。巧合的是，TLA中目标性质定义的语法和Rholang 0.1中类型定义的语法非常类似。事实上，名字空间逻辑中的类型、空间逻辑模型里的类型、TLA中的目标性质这几个都有相应的对应关系，都是非常有意思的数学概念。而Rholang名字空间逻辑上的推导类型的LADL算法（用分配律表示逻辑）是这些概念的一个推广，不光是数学上很有意思，在分布式系统的工程实现中也有非常重要的好处。
要理解LADL，需要知道上世纪三十年代就被发现了的柯里-霍华德同构（zh.wikipedia.org/wiki/%）：人们发现，Lambda演算和直觉逻辑的公式之间是紧密对应的，两者可以相互转换。直觉逻辑中的公式或命题可以对应成为Lambda演算中的类型。直觉逻辑中对命题的证明的推导（规约）步骤对应了Lambda演算中的beta规约。上世纪的90年代，Pi演算提出后，人们也进而发现用Pi演算中的进程代替Lambda演算中的项（Term）也得到同样的对应关系：一个进程要满足的逻辑命题等价于这个进程满足的类型。你的进程通过了一个类型检查，也就自然证明了这个进程满足对应的逻辑命题，从而实现了自动化的形式验证。（Atticbee注：Greg在接下来讲了很多LADL的知识，需要很多数学功底才能理解，所以略过很多细节。）
LADL（用分配律表达逻辑）是一种推导、检查类型的算法。注意有一些类型是不满足分配律的，比如列表，因为列表中元素存在次序关系所以不满足交换律。但集合这个类型是满足的。然而我们并不需要支持最通用的类型集合（那就太复杂了，很难快速、自动的求解），只需要支持一个尽可能大的子集就行。
所以LADL的思路是放弃了对最普遍的代数结构的支持，这就不用求解非常难解的问题了，转而只支持一个子集（Atticbee注：最普遍的情况非常难解，需要穷举各种状态的组合，计算量非常大。）用LADL有很多好处，首先，可以一键快速生成类型系统（Atticbee注：从而也实现了在这个子集上的代码的一键形式化证明）；然后，可以用来作为一个更好的查询语言。比如现有的github系统，你是无法根据代码的结构进行查询的。如果可能根据代码的结构和行为进行查询，那会使得程序员的效率大大提高。
|
楼主
标题置顶
标题高亮
