RChain的乾坤大挪移

形式化验证大伙都能做，以太坊也能。关键是成本，还有并发下的，多个合约机间的，分片间的形式化验证和单个合约单线程的验证，是两个完全不同的概念。形式化验证的层级：

1. 单合约，单线程

2. 多合约，单线程

3. 单合约并发

4.多合约协作+并发

5.多合约夸分片协作+并发

越来越难。图灵机体系由于指数爆炸，也就爬爬底下一两级。日链由于可组合性，爬到顶的难度和爬第一级的难度都是差不多的，没多大区别。

基于Rho演算构建世界计算机，是为了一下子搞定第5级的形式验证的。别的项目资质不行，只能练到乾坤大挪移第1层，咱们能练到第5层。

单线程下的形式化验证，一般就是霍尔逻辑那套，对每句代码抽象出前条件、后条件、命令，然后看一段代码能不能推导出所需要的断言。并发下的形式化验证，一般用TLA+之类的工具，先抽象出状态和状态转移，然后穷举，看看能不能得出不管路径怎么变都能得出希望的结果。这两种都不能扩展而且代价高昂。

第三就是不用状态穷举，直接进行数学推导，这就是进程演算的路子了。Rho演算没有状态，所有信息都包含在进程本身之中，进程的演变只有一条reduction规则，所以可以很方便的数学推导。LADL是其中一种数学推导的方法，快速生成类型，只要代码满足某种类型，自然满足了要求的性质，不需要穷举状态。

—-

编译者/作者：永春行

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。