协作：一份来自RChain的倡议书（上篇）

背景介绍

这不是一份普通的倡议书。一般倡议书会明确一个需要修复的市场部门，提供其规模大小相关数据，并在修复时提供财务预测。相反，本倡议所针对的是“人”，是为那些感到需要共同努力来度过未来艰难时期的人们而准备的。如果您不是这类人群，那么这就不是您所要寻找的。请无视之。

这段时期会有多艰难？据估计，全球已经失去了70％以上的昆虫（按生物量计）。请停止这个趋势吧。有多少不同的生态系统是依赖昆虫而生的呢？我们所谈论的不仅是像蜜蜂这样的授粉昆虫（而这已经足够具有毁灭性了），而是所有的昆虫。您对此会感到口腔发干、肠胃难受，这是地球上第六次大规模灭绝的预兆。

就连高盛也不得不承认全球气候变化的规模。如果没有那么被误导，他们关于如何能够从中获利的那些欢欣鼓舞的想法可能还会很可爱。尼尔·戴格拉斯·泰森（Neil deGrasse Tyson）在美国有线电视新闻网（CNN）上提到我们没有在未来20年内将沿海城市向内陆移动20英里的技术，他说的没错，但不要让这种观点误导您，让您认为气候变化仅仅是海平面上升而已。看看洛杉矶大火吧（例如华纳兄弟公司地块上的这场大火）。洪水将与大火一起到来。

饮用水也面临稀缺。印度地下的主要含水层已减少到原来的四分之一。由于冰川融化，它是不会恢复的。请考虑一下这对于该地区的可耕种土地意味着什么，然后以此类推。未来的耕地将大不相同，而这会对供应链管理产生巨大影响。

为避免误解，本倡议书并不能提供一劳永逸的解决方案。它所承载的是“希望”——一种超出理性的希望，为爱心所能产生的变革力开辟一方道路。尽管如此，本文所提到的所有内容仍然都将基于合理的数学基础而进行。理性和爱心、大脑和内心都是必须的，我们甚至还可能需要第三种力量：共同努力，以摆脱我们所造成的这种混乱状态。

协作技术

为了度过即将到来的几十年，并建立一个不是以“可持续”文化，而是以“可再生”文化为基础的世界，我们必须以人类历史上从未有过的方式进行协作。幸运的是，协作是智人的超能力。单凭一个无毛两足动物是无法抵抗猛犸象的，然而通过团队合作，早期的猎人成功灭绝了猛犸象。

到了现代，我们主要通过三种工具扩大了这种超能力：资本、治理和社会电信。不幸的是，所有这三种都需要重新启动了。资本的最初目的是帮助我们照料彼此并保护地球，然而它现在却被掌握在少数人的手中。无论您的政治立场如何，您都必须承认，这大大减少了我们在需要扩展协调方式时可用于资本探索的协调模型的数量。

由于互联网技术的存在，治理已处于变革压力之下。互联网技术使几乎每一个公民都能对政治行为进行核查与录像，从而使透明度和问责制迫在眉睫，对它们的抵制就等同于抵制真理本身。世界各国政府对此问题的应对措施太过缓慢，尽管科学共识已占据压倒性多数，但许多国家（例如美国）事实上仍然在否认我们所面临的生存危机，对已经发生的洪水、火灾和饥荒视而不见。他们无法及时代表其公民采取行动，原因就在于其中大多数人骨子里就已经被腐化了。

同理，集中化社交媒体（例如Facebook）已经达到了可以被外国势力用来影响主要民主国家选举结果这样的地步。此外，对这些滥用行为的严厉回应（例如Facebook频繁地改变审查制度）同样令人担忧。

自主身份、数据隐私和去集中化

最后一点一直是市场和公共部门所共同关心的问题。市场已经对少数集中公司在数字资产管理平台功能方面的主导地位做出回应，那就是寻求关键替代方案：自主身份、数据隐私和去集中化。这些追求都集中体现在被称为区块链的技术上。

#自主身份

市场越来越关注Facebook和Google在网络身份方面的主导地位。几乎所有在线服务都允许（实际上更偏好）通过Facebook或Google进行注册和登录。这就意味着这两家公司控制着网络上亿万人的在线身份。为了应对这种严重威胁在线独立性和个人隐私的状况，必须发展自主身份——这个术语的意思是人们应该自主识别身份，在任何特定的交流环境中只披露自己想要披露的内容。他们所披露的数据应通过加密服务和可信方网络（而不是任何单个的提供商）的组合进行验证。

#数据隐私

与自主身份一样，大型在线公司储存了无数个人信息的事实让市场对此正变得越来越焦虑。尤其是在过去几年中，这些公司出现了许多安全漏洞。许多术语已成为共识，这体现了日益加剧的公众焦虑。监视资本主义就是一个例子，它描述了一个事实，即消费者（及其个人数据）已经成为这些主要在线提供商向广告商以及更邪恶的代理机构（例如Cambridge Analytica，该公司被公认是英国脱欧投票的幕后策划并参与了唐纳德·特朗普的选举）所出售的产品。

许多部门都提供了针对个人数据保险库的解决方案，包括万维网的发明者蒂姆·伯纳斯·李（Tim Berners-Lee）。同时，公共部门也提出了相当严格的法规，例如欧盟的GDPR。

#去集中化

更广泛地说，市场一直在探索去集中化的替代方案，以构建在过去几十年中兴起并渗透进入现代生活的各种在线服务。其中以区块链最为突出。

所有区块链（至少是那些名副其实的区块链）的核心都是经济安全、无领导者的共识算法。本质上，这种算法（无论是工作量证明PoW、股权证明PoS 还是其他类型的算法）都可以使彼此不信任的计算机程序就价值达成协议。由于它们同意该值，因此可以存储本地副本以便于访问，并且仅在该值发生更改时才运行算法。如果具有足够的可扩展性，那么就可以以此体量来部署全球性的分散数据网络。

我们必须指出该发展的重要性。在线服务最近15年的发展都与数字资产管理平台相关，例如GitHub，Spotify，Facebook，Instagram，Twitter，Dropbox，GMail，Google Maps等。它们帮助数十亿人上传、传播和管理海量的数据。即使是第二波互联网服务（有时也称为共享经济），包括PayPal，AirBnB和Uber，也都与数字资产管理平台息息相关，通过平台可以连接到物理资产和其他种类的资产。

数据至关重要，它也会对我们应对气候变化的协调性需求产生影响。就像资金集中在少数人手中限制了可通过资本实施的协调模型的数量减少一样，数据集中在少数人手中也有可能会限制我们可通过数据和社会电信来实施的协调模型的数量。尽管许多在线数字资产管理平台都开始使用更为开放的模型，但它们每天都在变得越来越不开放。Google不再以“不作恶”作为座右铭，而Facebook也历经了好几波审查。当微软收购了GitHub，来自多个地缘政治地区的开发人员被剥夺了使用其代码的权利。

去中心化全球数据网络的出现代表了一个重大的转变。然而，区块链完全颠覆市场的潜力并不止于此。在开发出共识算法（也被称为工作量证明PoW）后，比特币网络选择使用其在比特币持有人的地址记录余额并存储分类帐。该选项具有明显但有限的实用性。对于共识算法存储，更先进的使用方法是虚拟状态机。该选项最初由以太坊构思和开发，旨在将全球数据存储转变为全球计算机。这台计算机没有实体，却无处不在。

区块链与可扩展性

当然，由区块链技术所构建的这些服务真正实现去集中化是基于可扩展性。如果我们要基于比特币和以太坊等工作量证明（PoW）型区块链对这一问题进行分析，那么得出的结论可能会是“不行，无法扩展”。工作量证明会花费过多计算周期，这实际上是浪费的。本质上，该协议是用热量换取了安全性，而且仅仅是相当微弱的安全性。

此外，即使工作量证明共识算法可扩展，以太坊所选择的虚拟机也是时序机，这意味着所有交易必须通过该机器按顺序进行。但是，大多数交易是隔离且同时进行的。在智利购买肉馅卷饼的人和在上海街头购买烤豆腐的人，他们所接触到的财务资源是不同的，他们的交易可以且确实是独立进行的。如果想要了解时序虚拟机的功能，可以联想一下八车道高速公路。当所有八通道都汇集成一条通道时会发生什么？更糟糕的是，由于它是按顺序的，当您向网络中添加更多服务器节点时会产生更多竞争，因此添加计算资源会导致网络变慢。

最后，即使这种虚拟机有扩展的可能性，这种平台（使开发人员能够在全球计算机上编写程序的平台）也会面临巨大的安全风险，即那些高度用户定义的智能合约。即使核心协议可以通过各种方式完美交付，但是由于在这台全球计算机顶部编写程序的是人类开发人员，他们总是会出错的。从一个1.5亿美元的资金池中抽取了5000万美元的DAO bug就是用户级代码而非核心协议代码的问题。而这些令人难以置信的破坏性错误目前相对较少的原因，只是因为现在还没有人在以太坊上构建重大应用程序，因为它没有扩展性。实际上，正是因为以太坊无法扩展，DAO bug本身才可以重现。想象一下，如果以太坊以4万笔交易/秒的Visa速度而不是以当时的10交易/秒的速度运行，网络上将会发生什么。

概括来说，区块链是在我们真正需要它的时候出现的。我们需要它的原因不仅仅在于全球对于资本和数据资产集中化的担忧，还因为气候变化对人类构成生存威胁，而我们需要重新启动协调基础结构来应对其后果。RChain就是在这样的背景下开发的：在至关重要的时间表下回应这些问题。

RChain：一种技术解决方案

RChain在提供其RNode系统时汇集了五种主要技术组件：

●Rspace：一种新型的键值存储

●Rholang：一种新型的编程语言

●Casper：一种新型的共识算法

●Behavioral types（行为类型）：一种新型的类型系统，以及用于为各种编程语言和计算模型生成此类型系统的LADL算法

●以及用scala实现p2p Kademlia通信和节点发现协议。

这些组件及其所实现的创新均旨在满足特定的市场需求。总体来说，RChain宁愿遵循有意义的艺术实践和工程设计，而不是将钱花在昂贵的现在已有的研发上。同时，RChain也认识到如果我们想要构建一个优秀到足以重建世界数据和金融网络的平台，则其必须与眼下大多数的互联网软件有所区别。

RChain对此有清醒的认知，因此它使用了一种截然不同的开发方法，有时也被称为按构造校正（correct-by-construction）。该方法从正确性证明（proofs of correctness）中提取程序，其最终目的是对运行其中的代码进行形式化验证，并证明它们是正确的。为了达成上述目的和目标，这种级别的软件质量和可靠性是必不可少的。

请注意，按构造校正（correct-by-construction）并不会回溯到软件开发的瀑布模型。也就是说，它并不需要等待数学或软件的完善。数学模型可能是内部一致且被证明是正确的，但由于它对生产会提出全新的或略有不同的要求，因此可能不适用于生产环境。经验丰富的数学家和软件开发人员都知道，证明和程序都只在准确建模和编码的框架内有效。在发展的市场中，对需求的深刻理解是反复进行的，就像在自然界中反复进行可行性适应一样。因此，按构造校正（correct-by-construction）完全适合于敏捷开发方法，这些方法都与管理软件开发的迭代性质有关。

技术分析

1. RSpace：一种新型的键值存储

在过去的十年中，技术社区（特别是那些涉及大数据的社区）已经对存储和检索进行了重新思考。尤其是围绕No-SQL替代关系数据存储的辩证法已经发展起来了。首先出现的是基于键值的存储系统浪潮以及map-reduce范式。随之而来的是强烈反对，就查询和交易的语义提出了对键值存储范式的批评。RSpace可以解决该问题，它提供了一种无SQL存储，同时仍然具有清晰的查询和交易语义。它还提供了一项支持查询中用户控制并发性所必需的关键功能：存储代码（code）和数据（data）的能力。实际上，将代码（code）和数据（data）放在存储层上的平等地位是源于一致性约束，该约束来自最古老的逻辑规则之一——排中律。为了避免这看起来过于偏向理论，重要的是要了解这是第三代技术。Meredith为Microsoft的BizTalk流程编排（业务流程自动化平台）设计了该版本，然后对其进行了更新，以在SpecialK中使用所谓的定界延续（delimited continuation），最后提出了RSpace设计作为对RChain扩展性的进一步改进。如需了解更多信息，您可以在RChain的GitHub代码库中浏览RSpace，就像RChain的所有软件一样，它也是开源的。

在前面的讨论中，我们明确了以分散方式组织和处理全球数据的需求，首先是要建立并完善我们在过去十年大数据中所学到的知识。本质上，从Google到Facebook，所有此类组件都是作为私有资产位于所有主要的数字资产管理平台中的。但其中最主要的区别是我们提供的是开源的软件，适合用于去中心化的公共基础设施中，而其特征和功能则源自rholang编程语言中所体现的特定并发语义。

2. Rholang：一种新型的编程语言

Rholang直接回应上述要求，即状态存储在区块链中的虚拟机（即计算模型）必须从根本上并发，而不是时序的。从图灵机到lambda演算，从Petri网到π演算的各种计算模型，分析表明市场需求包括四个属性。具体来说：

● 完整性——是否能表达所有需要表达的内容？

● 组合性——是否能从简单的程序中构建出更复杂的程序？

● 并发性——是否能构建部分同时运行的程序？

● 复杂性——能否衡量计算资源的成本？

以上表格显示，π演算（更广泛地说是为移动进程演算的一系列计算模型）是唯一具有全部四个特征的模型。同样，使用此表可以快速浏览市场上的大多数区块链项目，可以看到哪些项目需要扩展。如果它们不是基于具备所有四项功能的模型之上，则不具备可扩展性。

我们可以在此表中添加其他行：已用作支持上一代智能合约的企业级产品的基础；已用作指定上一代智能合约的互联网标准的基础。同样，只有π演算能够满足所有要求。具体来说，本倡议书的作者Greg Meredith是Microsoft BizTalk流程协作和XLang语言的首席架构师，XLang语言不仅是企业和互联网规模业务流程自动化的基础，还是许多W3C标准（包括BEPL和BPML）的基础，符合WS-Choreography标准。所有这一切都表明，选择使用像π演算这样的模型不仅在理论上合理，而且在实践上也合理，符合行业标准。

提到这个话题就不得不说，对并发性计算模型有要求的不仅仅只是区块链。互联网级别程序的编程模型需要迁移到并行计算模型，它们对此已经在相当长的一段时间内承受了很大的压力。在过去的二十年中，有两种趋势一直在从下方与上方对编程模型施加压力。下方压力来自于摩尔定律于2000年代初的终止。在上一个时代，开发人员编写完C代码就可以坐等一年，由于处理器速度的提高，代码性能就能翻倍。当2000年初时序处理速度达到极限时，这种趋势就结束了，而加速计算的主要方式是在每个裸片中放置更多的内核，每个盒子容纳更多的芯片，每个机架容纳更多的盒子，每个数据中心容纳更多的机架。不利用这种并发性的代码就无法扩展。同理，就像我们所讨论过的那样，互联网商业化需要的是可由数百万并发用户24x7全局访问的程序。同样，本质上非并发的代码是无法满足这种需求的。

这意味着用于对互联网级别应用程序进行编程的编程模型（无论它们是否精通区块链）必须是并发的。移动进程演算为这种发展奠定了基础，不仅因为它们代表了语言设计的重大进步，而且还因为它们为程序的静态分析奠定了坚实的基础。 很难说明此功能的重要性。并行编程比顺序编程要艰难许多倍。如果没有静态程序分析的大力支持，并发代码中的错误将随着编写并发代码的程序员数量的增加而变得不堪重负。

Rho演算与π演算 （Rho-calculus vs π-calculus）

如前所述，π演算只是一系列模型的一个例子，它具有市场所需的所有功能。自图灵奖获得者Robin Milner提出该模型以来，许多具有π演算特色的计算模型都已出现并投入研究，包括联接演算（join calculus）、蓝色演算（blue calculus）和环境演算（ambient calculus）等。其中每一项都各具特色，但最终都因各种原因无法进行映射或将互联网编程为π演算。然而，有一个从π演算派生而来的模型，它修复了一个小漏洞，同时又增加了一些在互联网编程中常见的强大功能，那就是Meredith和Radestock的Rho演算。

Rho演算通过将模型的名称（name）设为第一类元素，在π演算中开了一个洞。在名称理论（theory of names）中，π演算是参数化的；也就是说，给定名称理论，π演算将产生一种过程理论（theory of processes），该过程根据使用这些名称作为通道的通信来完成计算。对于π演算来说，无论该名称是电话号码、电子邮件地址、区块链地址还是以上所有名称都可进行。但是，纯π演算只能在进程之间交换名称，就像人们通过交换电话号码完成任务一样。事实证明，尽管理论上可行，但这需要大量工作！但是，互联网不只是数据（data），代码（code）存在于每一个进程（process）中，而rho演算则完全支持此功能。

名称空间和分片（Namespaces and Sharding）

Rho演算通过使名称（name）成为过程代码（process）来实现运送过程。一旦名称被编码，就可以将所有不同种类的地址的常见电信概念编码到rho演算设置中，无论是电子邮件或区块链地址都可以完美嵌入，因此能将最常见的寻址方案嵌入到互联网：URI和URL。后者之所以重要，不仅因为它是整个万维网的组织方式，也因为它标志着rho演算改进的一项强大功能：名称空间（namespace）。URI将网络组织成一棵资源树（实际上是森林，但是用树木指代就足以满足讨论了）。每一个URI都是从树木根部沿着分支进行到保留资源的叶或端点的一条路径。基于这种路径结构，仅使用部分路径就可以指示整个资源组或空间，这就允许我们用树和路径结构来组织和搜索资源空间。Rho演算通过以编程方式识别这些空间，从而将此范例更提升一个级别。

此功能对市场而言之所以如此重要，原因还是因为大多数交易都是孤立的。我们需要一种编程方式来细分、组织和重新组织这些交易，以便根据共有的资源对它们进行分组。这通常被称为区块链空间中的分片（sharding），而rho演算名称空间（namespace）功能则提供了一种非常强大的分片方法。具体来说就是可以使用相同的方法重新加入分叉，与其他网络进行互操作，并提高独立交易的速度。

操作语义和按构造校正的语言设计（Operational semantics and correct-by-construction language design）

为了讨论的完整性，按构造校正方法和rholang语言系统之间的相互作用是必不可少的。Rholang编程语言的语义是基于最佳实践而构建的。Rho演算为rholang的核心功能提供了图灵完备操作语义。Rholang的所有附加功能都是通过映射回核心演算来定义的，这意味着该语言是按构造校正的。与以太坊的Solidity和EVM相比，Solidity还没有正式的语义。而当它最终获得正式语义后，它将有义务证明生产中的任何编译器都应以保留语义的方式将Solidity编译为EVM字节码。如果没有这样的证明，那么怎样的防护措施才可以防止字节码注入攻击（bytecode injection attacks）呢？谁能告诉我们攻击者的编译器没有发出将少量以太币虹吸至其帐户的字节码呢？

Rholang不会遭受这样的攻击，因为它的语言和执行机制（简称RSpace！）都直接源自rho演算，这就是按构造校正法所带来的好处。还需要注意的是，我们怎样才能在不必了解与分布和共识有关的更广泛的市场要求的前提下从中受益呢？这就回到了我们早先提出的观点，即按构造校正法更适合迭代和敏捷的需求收集和开发流程。

除此以外我们也要意识到，必须使用干净的操作语义来明确一个程序何时可以替代另一个程序。换句话说，什么时候在更广泛的执行上下文中放入一个不同的程序来代替另一个程序才是安全的呢？这个概念可以追溯到Liskov的可替换性原则，从长期维护系统的实际角度来看，这是一个关键特性。您需要知道何时可以为旧组件或故障组件交换升级或修补程序。在软件中，这取决于具有编程语言的语义，而操作语义（operational sematics）是迄今为止在理论和实践中最广泛使用的编程语言语义的形式。

这种可替换性原理与静态分析密切相关，尤其是通常称为类型检查（type checking）的静态分析形式。根植于特定类型中的所有程序在所有需要该类型的任何上下文中都可以被替换，这是即插即用（plug-n-play）软件的基础，适用于所有正式的生产环境。但是，大多数流行的现代语言的类型系统（type system）都相对较弱，仅确保提供的数据结构与预期的数据结构匹配。他们没有明确的程序结构，更不用说程序行为了。在过去的二十年中出现了一类新的类型系统，但它尚未进入主流编程语言。而Rholang的行为类型则旨在改变这种状况。

3. Casper：一种新型的共识算法

在区块链之前，特别是在工作量证明（PoW）之前，像PAXOS这样的分布式共识算法更倾向于锁定一致性而不是可用性。从规模上讲，这种选择是行不通的，几乎所有的全球平台（例如Facebook和Twitter）使用的都是某种形式的最终一致性。区块链在此基础上进一步发展，并将其锁定在一个更加激进的想法上：通过经济的方式保护协议，而其秘诀则是使攻击网络的成本过高。长期以来众所周知，对基于工作量证明的网络进行“不可能的” 51％攻击不仅是可能的，而且已经在著名的工作量证明网络上发生过了。然而，提高攻击代价的想法仍然是有效的，只是不应该将时间浪费在猜测数字并以此作为工作证明的手段上。

相反，人们可以继续采用按构造校正（correct-by-construction）方法并遵循逻辑。在80年代末和90年代初，吉拉德的线性逻辑彻底改变了我们关于逻辑和证明的观念。具体而言，线性逻辑对资源相当敏感。不同于命题A&A与命题A相同的经典逻辑或直觉逻辑，线性逻辑考虑的是建立命题所需的资源。可以从建立化合物特性的方面来思考。鉴定化合物具有给定性质的许多测试方法都需要调整甚至破坏一定量的化合物。说白了，在古典逻辑中，“我有一个美元”&“我有一个美元”对可能意味着“我有两个美元”的可能性并不敏感。事实上，有效的线性证明必须仔细考量所有资源并防止重复支出。毋庸置疑，我们可以使用线性逻辑来寻找有关共识的线索，尤其是经济上有保障的共识。

在线性逻辑的不同语义中，游戏语义既直观又具有多能性，其许多变化都能够说明线性逻辑的各种特征。Hyland和Ong的游戏语义能够对逻辑进行直观阐述。在Hyland-Ong游戏的语义中，玩家和对手的每一个动作都必须由先前的动作来证明，而这种语义结构就是其用来建立策略的单线程性。Greg Meredith在2009年提出使用这种结构来保护早期版本RSpace（称为SpecialK）实例之间的通信中的网络协议安全。根据这些见解，CBC-Casper在区块上加强并利用了一种合理化结构来检测模棱两可性，且它提供了活跃性约束和公平性约束。通常我们可以通过施加某些通信模式来确保这些属性，而证明结构则可以帮助了解通信历史，以便可以检测其特性或其违反情况。

通过使用可靠的检测违规的手段，我们可以在经济上确保权益证明的有效性。参与者加入了用于防止拒绝服务的代币并削减了其份额，一旦违反合同，其份额将会部分耗尽或被完全没收。从长远来看，只有遵守规则的参与者才能留在游戏中。这比浪费时间猜测数字要有效得多。

4. 行为类型（Behavioral types）

2005年的论文《名称空间逻辑》（Namespace logic）描述了rho演算中程序的逻辑和类型系统。这些类型可用于描述各种现象，比如用来确保进程只能并且仅在特定范围通道上通信的编译时的防火墙、确保进程不会卡死的无死锁 、以及用于通用数据格式（例如XML模式）的编码。其逻辑是Brouwer直觉数学计划（Intuitionistic mathematics programme）发展的一部分，该计划坚持认为证明数学对象需要构造数学对象，而不是通过荒谬的还原论证来进行推断。其他亮点还包括：Curry和Howards对lambda演算中的简单类型的回应以及直觉逻辑中的公式；以逻辑形式出现的阿布拉姆斯基（Abramsky）领域理论；罗宾·米尔纳（Robin Milner）和马修·轩尼诗（Matthew Hennessey）的进程计算模态逻辑；Caires的空间行为逻辑；吉拉德（Girard）的线性逻辑；以及Wadler的会话类型。这是一个漫长而杰出的发展过程，而编程语言设计师只挖掘了其中的一部分。

Rholang完全接受该方法。Greg Meredith在2015年对Vitalik Buterin和以太坊社区所有人提出警告，该平台——任何智能合约平台——的主要安全隐患都在于用户定义的合约。在警告提出后不久，以太坊就被DAO合同中的一个bug击中。DAO智能合约是实施去中心化初创项目的平台。该想法大受欢迎，价值1.5亿美元的ETH被发送到了合约中。但攻击者发现了一个漏洞，并从合约中盗取了大约5000万美元。幸运的是，以太坊仅以约10笔交易/秒的速度运行，否则所有1.5亿美元都将在几秒钟内消失。

在该bug被报道后，Greg Meredith和Pettersson马上证明了如果将错误的合约用rholang语言编写并进行行为验证，相应地，有问题的代码永远不会被编译，更不用说被检入和应用了。在rholang中，该bug会显示为在更新合同状态与处理下一个客户请求之间的竞争，它能够访问陈旧状态。来自名称空间（namespace）逻辑的类型会捕获竞争条件。比起为以太坊的智能合约语言Solidity开发该类型系统的价格，他们所蒙受的价值损失和社区动荡是其代价的十倍以上。这就是为什么我们要以该类型系统启动RChain的原因所在。

逻辑作为分配法则（Logic as a distributive law ：LADL）

行为类型方面的许多发展表明，生成类型系统的算法是存在的。由Greg Meredith和Mike Stay开发的LADL（Logic as a distributive law）算法就是这样的算法。假设

● #可以在JVM的规范中找到或者在标准ML的语义或rho演算中找到的一种计算概念，以及

● #集式集合的概念（a notion of a set-like collection），以及

● #显示如何将开洞术语归结为通过填充洞而形成的术语集合的分配法则（a distributive law, which shows how to term with a hole in it into a collection of terms made by filling the hole）

LADL会生成一种类型系统，这种类型系统比Java，Haskell或Scala中的类型系统丰富得多。它可以看到旧程序类型系统所无法了解的程序结构和程序行为的信息，而对于程序的相关子集来说是可以确定的。

由于这种丰富性，这些类型也可以被视为查询语言。如果数字资产管理作为全球协调技术是互联网的基石，那么就有一种既至关重要又极为不足的数字资产，那就是代码（code）。代码是互联网的难题。它负责大部分功能，作为数据资产受到存储和管理，但是对于结构化数据的标准查询机制却是不透明的。而行为类型则允许我们过滤代码，即根据结构和功能来选择代码。这种功能不仅彻底改变了GitHub之类的服务，还为智能合约平台奠定了成功条件——该平台使人们能够从数十亿种可能性中找到所需，足以托管数十亿份智能合约。

（未完）

————————————————————————————————————————

作者介绍：

Lucius Gregory Meredith

分布式计算的先驱，RChain创始人，Rho 演算的发明人

Greg在英国帝国理工学院获得分布式计算博士学位

曾担任微软 BizTalk 项目的首席架构师和微软 Highwire项目的首席架构师，参与制定了微软“下一代Web服务战略”

曾任微软CTO办公室顾问，微软高性能计算组顾问

BizTalk是微软的企业级旗舰产品，排名全球第一的集成解决方案，拥有上万个企业级客户

—-

编译者/作者：RChain官方

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