Actors, 元组和π演算

Rosette

MCC的Carnot研究小组在网景公司成名整整十年之前就已经预测到了互联网的商业化。然而，Carnot小组专注于去中心化、分布式的应用，并且研发出了一个称为可扩展服务网关(Extensible Services Switch,EXX)的网络应用结点，以及用于在这些结点之上编程的编程语言Rosette。 而Rosette/ESS的研究模型则是actor模型。在这里，我们特别讲述了由Carl Hewitt开发并由Gul Agha精炼的模型，Gul Agha之后为Rosette的设计提供了建议。

Rosette在作用域和优雅上的成果令人瞩目。尤其是，Rosette把一个actor分解为

  • 一个邮箱(一个接受actor客户端消息的队列)
  • 一个状态(许多值组成的元组)
  • 元信息(描述如何通过更抽象的关键字访问状态值)
  • 以及一个共享的行为对象(一个从消息类型到响应时需要运行的代码的映射，大致相当于C++语言中的vtable)

Actor的处理过程包括从邮箱中读取下一条信息，使用共享的行为对象(share behavior object, sbo)来确定使用哪些代码来执行而得到针对该消息的响应，然后在执行环境中运行代码，在该执行环境中元信息所引用的键被绑定到状态元组对应的位置。该代码主要将消息发给其他actor，之后可能在等待响应。

Actor通过更新在并发运行中提供一个一致的状态视图，更具体地说，一个actor直到它被更新之后才会处理邮箱中的下一条消息，并且当actor正在处理当前消息时，邮箱上锁并且将进来的客户端请求排队。当一个actor调用了更新操作，一个新的逻辑线程将被创建来处理邮箱队列中的下一条信息。线程对该actor状态的视图全部都提供给了该次更新。前面的线程可能仍然会对状态进行更改，但是这些对后面处理邮箱中后续消息的线程都是不可见的，因此对后续的客户端请求也是不可见的。这种方法提供了一种可伸缩的并发概念，从消息抵达顺序不确定的单线程容器，扩展到某些系统级支持逻辑线程映射的外部容器(例如虚拟机，操作系统或硬件本身)。

这已经是一个比当今大多数工业系统中存在的acotr模型（比如Scala的AKKA框架）更具表达能力的模型。然而，Rosette模型更加优雅的是它对元编程的全部承诺。在Rosette模型中，一切都是actor。特别是，actor的邮箱是actor，而邮箱，状态，元信息和sbo都是actor。值得注意的是，Rosette使得这个完全反射模型具备退化到与Java或C＃等语言相同或更好性能的可能性。

从某种意义上说，Rosette模型中的actor的结构化反射也在Java这样的语言中得到了体现，在这些语言中，类也可以通过编程方式探查和参与计算的对象。然而，Rosette将反射原理更进一步。该模型不仅提供了结构化反射，而且还提供了程序化反射，通过提供与模型中固有的并发性相一致的延续的概念。具体而言，就像移位复位风格的分隔延续表示中的使用移位块使得等待延续可用在代码块中一样，Rosette的反射方法使得等待延续可用作方法的参数。稍后再说。

结束这个简短的总结笔记：Rosette不仅仅是结构上和程序上的反射，更是词法上的反射。也就是说，Rosette程序中的所有句法结构也都是actor！反射式的底层构造为干净的宏系统、嵌入式领域特定语言以及其他语法和符号处理特性提供了基础，而这些是许多工业语言在Rosette完成20年后还难以提供的特性。

元组空间

大约在Rosette模型被研究用于在去中心化和分布式环境中开发应用的同时，Gelernter提出了Tuplespaces。他的想法是在互联网的物理层和通信层之上创建一个逻辑仓库。该仓库基本上被组织为分布式键值数据库，其中键值对被用作计算之间的通信和协调机制。 Gelernter描述了与元组空间交互的三个基本操作： out 用于在元组空间创建一个新的数据对象，in 从元组空间消费（移除）一个对象，以及 rd 读取一个对象并且不移除它

与消息传递系统不同的是，这种方法允许发送者和接收者在彼此不知情的情况下进行操作。当一个进程产生一个其他进程所需要的结果，它只是将新的数据转储到元组空间。需要数据的进程可以使用模式匹配在元组空间中查找它。

out("job", 999, "abc")

in("job", 1000, ?x) ; blocks because there is no matching tuple
in("job", 999, x:string) ; takes that tuple out of tuple space, assigning 'abc' to x

这引起了关于如何发布持久化数据的问题，以及进程悬停等待元组空间中不存在的键值对时会发生什么情况的问题。此外，元组空间机制对编程模型没有任何限定。使用元组空间的代理可以用各种各样编程模型来编写，这些编程模型对并发语义具有各种实现和解释器。这使得在由许多代理通过元组空间进行交互的应用程序中进行端到端语义的推理变得尤其困难。然而，模型在沟通和协调上的简单性已经引起了广泛的关注，在随后的几十年里，关于元组空间的实现产生了很多。

元组空间概念与actor模型之间的显着区别在于actor模型基本端口的限制。一个actor有一个位置，即它的邮箱，监听世界其他地方的行为。现实中的系统和现实中的系统开发通常要求应用程序需要监听两个或更多的数据源并在它们之间进行协调。例如，Fork-join的程序，会spawn出多个程序对多个数据源请求信息，然后后续的计算过程将这些来自自动化数据源的结果信息流合并，这种算法是人类决策过程中一种常见的想法，应用于诸如从贷款处理，到学术论文的审查。当然，可以安排一个actor在多个actor之间进行协调，然后负责这些独立的数据源的处理。但这在应用程序中引入了开销，并打破了封装，因为参与者必须要知道他们正在被协调。

相比之下，元组空间模型非常适合协调跨多个自动化数据源的计算过程。

移动进程演算的分布式实现

Tomlinson，Lavender和Meredith等人提供了Rosette/ESS中的元组空间模型的实现，作为进行两种模型研究的手段，并比较两种风格所写出来的应用程序。正是在这项工作中，Meredith开始了对移动进程演算的深入研究，并把他作为actor模型和元组空间模型的第三个替代方案。主要需求之一是在具有一个统一的编程模型（如Rosette的actor模型）之间建立桥梁，通过元组空间模型提供的简单但灵活的通信和协调概念，使应用语义的推理变得容易得多。

在下面描述的代码中，方法名使用consume和produce来代替传统的Linda动词 in 和 out 。原因在于，一旦使用了反射法策略，然后使用划定的延续进行细化，这会导致与数据和延续生命周期相关的新的重要观测。

元组空间get语义的Rosette实现
(defRMethod NameSpace (consume ctxt & location)
 ;;; by makng this a reflective method - RMethod - we gain access to the awaiting continuation
 ;;; bound to the formal parameter ctxt
 (letrec [[[channel ptrn] location]
                ;;; the channel and the pattern of incoming messages to look for are destructured and bound
        [subspace (tbl-get chart channel)]
                ;;; the incoming messages associated with the channel are collected in a subtable
                ;;; in this sense we can see that the semantic framework supports a compositional
                ;;; topic/subtopic/subsubtopic/… structuring technique that unifies message passing
                ;;; with content delivery primitives
                ;;; the channel name becomes the topic, and the pattern structure becomes
                ;;; the subtopic tree
                ;;; this also unifies with the URL view of resource access
       [candidates (names subspace)]
       [[extractions remainder]
          (fold candidates
            (proc [e acc k]
                (let [[[hits misses] acc]
                [binding (match? ptrn e)]]
            (if (miss? binding)
                (k [hits [e & misses]])
                (k [[[e binding] & hits] misses])))))]
                  ;;; note that this is generic in the match? and miss? predicates
                  ;;; matching could be unification (as it is in SpecialK) or it could be
                  ;;; a number of other special purpose protocols
                  ;;; the price for this genericity is performance
                  ;;; there is decent research showing that there are hashing disciplines
                  ;;; that could provide a better than reasonable approximation of unification
       [[productions consummation]
            (fold extractions
              (proc [[e binding] acc k]
                (let [[[productions consumers] acc]
               [hit (tbl-get subspace e)]]
                  (if (production? hit)
               (k [[[[e binding] hit] & productions] consumers])
               (k [productions [[e hit] & consumers]])))))]]
                  ;;; this divides the hits into those matches that are data and
                  ;;; those matches that are continuations
                  ;;; and the rest of the code sends data to the awaiting continuation
                  ;;; and appends the continuation to those matches that are currently
                  ;;; data starved
                  ;;; this is a much more fine-grained view of excluded middle

   (seq
     (map productions
       (proc [[[ptrn binding] product]]
            (delete subspace ptrn)))
     (map consummation
          (proc [[ptrn consumers]]
            (tbl-add subspace
            ptrn (reverse [ctxt & (reverse consumers)]))))
     (update!)
     (ctxt-rtn ctxt productions))))
元组空间put语义的Rosette实现
;;; This code is perfectly dual to the consumer code and so all the comments
;;; there apply in the corresponging code sites
(defRMethod NameSpace (produce ctxt & production)
 (letrec [[[channel ptrn product] production]
        [subspace (tbl-get chart channel)]
       [candidates (names subspace)]
       [[extractions remainder]
          (fold candidates
            (proc [e acc k]
                (let [[[hits misses] acc]
                [binding (match? ptrn e)]]
            (if (miss? binding)
                (k [[e & hits] misses])
                (k [hits [e & misses]])))))]
       [[productions consummation]
            (fold extractions
              (proc [[e binding] acc k]
                (let [[[productions consumers] acc]
               [hit (tbl-get subspace e)]]
                  (if (production? hit)
               (k [[[e hit] & productions] consumers])
               (k [productions [[[e binding] hit] & consumers]])))))]]
   (seq
     (map productions
       (proc [[ptrn prod]] (tbl-add subspace ptrn product)))
     (map consummation
       (proc [[[ptrn binding] consumers]]
       (seq
            (delete subspace ptrn)
            (map consumers
              (proc [consumer]
                (send ctxt-rtn consumer [product binding])
                binding)))))
     (update!)
     (ctxt-rtn ctxt product))))

本质上，该问题是，在输入请求满足输出请求后数据和延续这两个中的一个或两个会发生什么。在传统的元组空间和π演算语义中，数据和连续都从仓库中移除。然而，事件发生后，完全有可能将其中一个或两个都留在仓库中。每个独立的选择都会导致不同的编程范式。

Traditional DB operations

移除延续，但留下数据构成一个标准的数据库读取：

 

易失性的-data

易失性的-k

持久化-data

易失性的-k

易失性的-data

持久性的-k

持久化-data

易失性的-k
生产者 put store publish publish with history
消费者 get read subscribe subscribe

Traditional messaging operations

将数据移除的同时将延续保留，组成pub/sub模型中的订阅

 

易失性的-data

易失性的-k

持久化-data

易失性的-k

易失性的-data

持久性的-k

持久化-data

易失性的-k
生产者 put store publish publish with history
消费者 get read subscribe subscribe

Item-level locking in a distributed setting

标准的移动进程演算和元组空间语义将数据和延续都移除

 

易失性的-data

易失性的-k

持久化-data

易失性的-k

易失性的-data

持久性的-k

持久化-data

易失性的-k
生产者 put store publish publish with history
消费者 get read subscribe subscribe

在Tomlinson使用Rosette的反射方法来模拟元组空间语义（见上面的代码）的基础上，Meredith通过线性延续提供了从π演算到元组空间语义的直接编码。这种语义是微软BizTalk的Process Orchestration引擎的核心，微软的XLang可以说是第一个互联网规模的智能合约语言，而它正是由此产生的编程模型。这个模型直接影响到W3C标准，如BEPL和WS-Choreography，并催生了整整一代的业务流程自动化应用和框架。

与Rosette为actor模型带来的改进一样，π演算为应用程序提供了一个特定的本体论，这些应用程序是以通过消息传递信道进行通信的进程概念而构建的。重要的是要注意，进程是通道中的参数，而Meredith使用这个抽象层次为XLang中提供了各种信道类型，包括绑定到微软的MSMQ消息队列、COM对象和许多其他在当时的流行技术的接入点。也许当今互联网最核心的抽象在于，URI提供了一个自然的信道概念，允许通过URI感知通信协议（如http）实现编程模型。同样，就当今的存储地带而言，键值对存储(如nosql数据库)中的键也直接映射到π演算中的通道概念，而Meredith使用这个构想来提供π演算到元组空间语义的编码。

从元组空间到 π演算

π演算赢得了基于消息传递交互来构建的并发计算的核心模型。它在并发和分布式计算中所扮演的角色，就像lambda演算在函数式语言和函数式编程所扮演的一样，给出了计算的基本本质，并将其转化为可以执行计算的语法和语义。给定信道的一些概念，它构建起了一些基本的进程公式，其中前三个是关于I/O的，描述了消息传递的行为。

  • 0 表示惰性或已停止的进程，是模型的基础情况
  • x?( ptrn )P 表示输入看守进程正在监听信道 x ，等待与模式相匹配的消息，然后当接收到该信息后，会接着执行:code:P，其中模式中的所有变量被绑定到消息中对应的值。
  • x!( m ) 表示在信道 x 发送消息 m

接下来的三个表示进程的自然并发情况、信道创建和递归情形。

  • P|Q 表示由两个进程P和Q并行组成的进程，这两个进程是并发执行的。
  • (new x)P 表示一个执行子进程P的进程，在它的上下文中，x被绑定到一个新的信道，不同于所有其他正在被使用的信道
  • (def X( ptrn ) = P)[ m ] 和 X( m ) 表示进程的递归定义和执行

这些基本公式可以用元组空间里面的操作来模拟:

P,Q ::=                     [[-]](-) : π -> Scala =
    0                       { }
    | x?(prtn)P             { val ptrn = T.get([[x]](T)); [[T]](P) }
    | x!(m)                 T.put([[x]], m)
    | P|Q                   spawn{ [[P]](T)  }; spawn{ [[P]](T) }
    | (new x)P              { val x = T.fresh("x"); [[P]](T) }
    | (def X(ptrn) = P)(m)  object X { def apply(ptrn) = { [[P]](T) } }; X(m)
    | X(ptrn)               X(ptrn)

单子结构化的信道抽象

接着Meredith在两个方向上追求特性的提升。它们都与信道抽象有关。两者中的第一个将信道抽象与在反射编程范式中变得如此受欢迎的流抽象相关联。具体而言，很容易证明异步π演算中的信道对应于无限持久化队列。这个队列可以被视为一个流，并且是可以被单子化处理访问的流，就像在响应式编程范式中所做的那样。这为在前面提到的，支持人类决策应用的常见的fork-join并发模式添加了自然语法和语义的优势。

( let [[data (consume ns channel pattern)]] P)

for( data <- ns.consume(channel, pattern) ){ P }

这一点值得更详细的讨论。虽然π演算确实解决了actor模型的主要端口约束，但它并不为fork-join模式提供自然的语法和语义支持。π演算的一些变体，例如连接演算，已经被提出来解决这种困境，但可以说，这些提议深受一些特性纠缠，使得它们不适用于许多分布式和去中心化编程设计模式。同时，通道的单子解释提供了π演算语义中更为集中和基本的重构，这些与模型中所有现有的标志语义相一致，提供了fork-join的自然概念，同时也清晰地映射到响应式编程范式，从而使诸如Apache Spark等开发栈的集成相对简单。

如果我们从编程语言演化的角度来看待这个问题，我们首先看到的语义重构看起来像：

P,Q ::=                     [[-]](-) : π -> Scala =
    0                       { }
    | x?(prtn)P             for( ptrn <- [[x]](T) ){ [[P]](T) }
    | x!(m)                 T.put([[x]], m)
    | P|Q                   spawn{ [[P]](T)  }; spawn{ [[P]](T) }
    | (new x)P              { val x = T.fresh("x"); [[P]](T) }
    | (def X(ptrn) = P)(m)  object X { def apply(ptrn) = { [[P]](T) } }; X(m)
    | X(ptrn)               X(ptrn)

其中for-comprehension是使用延续单子的语法糖。这条成功的解析表明了对解释器中**源**的重构。

P,Q :: = 0
         | for (ptrn <- x)P
         | x!(m)
         | P|Q
         | (new x)P
         | (def X(ptrn) = P)[m]
         | X(ptrn)

这个重构出现在Meredith和Stay关于π演算的高阶范畴论语义的工作 [SM15] 中，之后在rholang设计中加入。需要注意的重要一点是，基于for-comprehension的输入现在可以平滑地扩展到来自多个源的输入，在继续被调用之前，每个或所有这些输入都必须通过一个过滤器过滤。

\[for( ptrn_{1} \leftarrow x_{1}; \dotso; ptrn_{n} \leftarrow x_{n} if cond )P\]

使用for-comprehension允许单子化使用的信道可以使用输入守护语义来规范参数，因此特定的join语义可以多形地提供。这个意义怎么强调都不为过。特别是:

  • 与join与递归不可分割地绑定在一起的join演算不同。单子守卫输入允许匿名的、一次性合并，这在人类决策过程中是非常标准的fork-join模式。
  • 它提供了用于模拟Kiselyov的LogicT单子转换器的适当配置。搜索每个输入源直到找到满足条件的输入元组，对每个输入源中的发散很敏感。更重要的是，公平的交叉是一个描述交织策略的编程算法，它对于可靠，可用和高性能的服务至关重要。这是LogicT的实际导入和在机器部署中的正确设置。
  • 我们现在有一个嵌套事务的语法形式。具体来说：P 只能在满足与输入源状态变更和条件相符的上下文中运行。此外， P 可以是又一个输入守护进程。因此程序员或程序分析器可以 依照句法地 检测事务的边界。这对涉及金融和其他关键任务的事务的合约至关重要。

前RChain智能合约模型

正如rholang设计中所规定的的那样，这是一个用于智能合约的RChain模型的前身。它为构造合约提供了迄今为止最丰富的通信原语集合，这是由理论和工业规模的开发和部署所共同推动的。然而，整套合约原语适合在一条线上。从基于PoW的区块链到EVM，在这个领域没有一个单一设计方案能够承受这个方案所经受的质量保证压力。具体来说，这个方案在所有使用Rosette、Tuplespaces和BizTalk的经验中都有所取舍，并将它们归结为一个单一的设计方案，该方案满足所有这些场景中发现的迫切需求。它只有七个原语，并且与当前市场的主要编程范例相符。然而，作为来自rholang规范的例子，以及用行为类型显示来防止 DAO bug的研究，现有区块链技术中可表达的全部合约范围都在此模型中被紧凑地表达。

然而, 正如在 rholang 设计中所看到的, 这只是故事的开始。为了理解在开发引入的这些概念，需要一些背景知识。在过去的20年里, 一场革命已在计算机科学和逻辑学中悄然发生。许多年来人们都知道, 对于函数式编程模型中的小而增长的代码片段中，类型对应于命题, 证明对应于编程。如果这种对应，五花八门地被称为类型即命题范式或Curry-Howard 同构, 可以被用来涵盖模型中的一个重要而实用的部分, 它对软件开发有着深远的影响。至少, 这意味着, 类型检查程序的标准实践与程序证明在执行过程中拥有一致的某些属性。与Curry-Howard 同构所覆盖的初始片段相关的属性，主要与相关形式的函数中输入输出数据有关, 通过编译时检查，有效地消除了这类内存访问违规的行为.

加上J-Y Girard的线性逻辑的发明，我们可以看到命题即类型范式的一个具体扩展。通过线性逻辑，我们看到了范围涵盖远远超过严格串行的函数式模型。类型检查所提供的作用范围从属性证明扩展到并发环境下的协议一致性检查。接着，Caires和Cardelli发现了空间逻辑，其进一步扩展了作用范围，包括程序内部形态的结构化属性。在这些发现的基础上，Stay和Meredith确定了一个算法，即LADL算法，来生成类型系统，带来了一系列从安全性、可用性到安全性质的结构化和行为化的特性。通过应用Stay和Meredith开发的LADL算法，这里介绍的无类型的合约原语模型被赋予了一个完备的类型系统，它足以提供一些编译时守护，保证处理金融财产和其他敏感内容的关键任务所要求的关键的安全性和可用性。一个在编译时守护的简单例子是足以在编译时去发现和防止在The DAO事件中引起5千万美元损失的bug。

SpecialK

信道语义的单子处理就是在SpecialK栈研究中的亮点。首先，它将信道访问映射到for-comprehension风格的单子结构化的响应式编程。其次，它将信道同时映射到与整个节点相关的本地存储，以及节点之间的基于AMQP服务提供商的通信基础设施中的队列。这提供了内容传送网络的基础，该网络可以在通信节点的网络上实现，其与基于π演算的编程模型集成。特别的，从以上代码的注释中可以看出，信道加模式的单子化对待统一了消息传递和内容交付编程范式。具体来说，信道可以被看作是主题提供者，而模式为消息流提供了嵌套的子主题结构。这整合了所有的标准内容寻址机制（例如URL + http），同时提供了一个查询模型。详细信息请参见下面的章节。

从SpecialK到RChain

正如我们将看到的，RChain合约模型继承了SpecialK对待内容交付的所有优点。但是，SpecialK所实现的前RChain合约模型是以嵌入领域专用语言作为Scala的一组类库，而RChain则将该模型实现为全面的编程语言，运行在区块链上复制的虚拟机上，极具以太坊的架构和设计理念。该选择解决了第一个Synereo白皮书中指出的几个Synereo 版本1中体系结构的缺点。特别是避免了为运转注意力经济学的财务能力而必须支付给其他区块链费用从而在注意力经济系统合约上遭受了许多基于经济上的攻击的问题。它还解决了与SpecialK语义中心的Scala有限的延续库有关的SpecialK技术栈中的技术债务问题，同时显着提高了其支持的智能合约的能力。

Rho演算

尽管单子抽象提供了在信道上用于内容流流动的结构，但更基本的观察提供了支持工业级元编程的必要结构。我们知道几乎所有的主要编程语言都支持元级编程。原因很简单，程序员不写程序，程序编写程序，程序员编写写程序的程序。这就是为何能在互联网规模上完成如此巨大的编程任务的原因，使用计算机尽可能地自动完成任务。从文本编辑器到编译器，到代码生成器，到AI，这些都是生产出互联网规模上运行的服务代码的基本生态系统的一部分。

从更狭隘的角度来看，观察到Scala在语言设计之后艰难的添加元编程特性的教训是很有用的。在Scala中的反射甚至在好几年间都不是线程安全。可以说，这次教训，再加上类型系统的问题，都是其设计之初不定的编译器和新语言设计的原因。这些以及其他经过深入探索的努力清楚地表明，从编程语言的核心设计开始时就提供元编程模型原语，对其寿命和实际应用都是很重要的。简而言之，一个实际上支持元编程的设计在想要获得与Java，C#或者Scala等同的生产完备特性的项目中更具成本效应。

从Rosette对元编程设计的总体承诺中得到一个线索，高阶反射π(r-eflective h-igher o-rder π-calculus,简写为rho-演算)，引入反射作为其核心模型的一部分。它提供了两个基本原语，反射和修改，允许正在进行的计算将进程转变为一个通道，将一个从进程修改后得到的信通转变回它所修改的进程。该模型在过去的十年间经历过多次同行评审。原型系统已有将近十年的历史，清晰得演示了其健壮性。它采用总数达到了9个的合约构建原语集合，远远少于以太坊智能合约语言Solidity，然而这个模型比Solidity更具表达能力。特别是基于Solidity的智能合约不享有内在并发。

资源地址、内容传递、查询和分片的启示

在深入研究模型与资源寻址，内容交付，查询和分片的关系之前，让我们先快速地看一下基于路径的寻址。请注意，路径并不总是能够合并。比如`/a/b/c`和`/a/b/d`。这些不会自然地合并成一条路径。然而，每一条路径都是一棵树，而这些树合并了一棵新的树`/a/b/c+d`。换句话说，树为资源寻址提供了一个可组合的模型。这也可以作为查询模型。要看到这个声明的后半部分，让我们用这种形式重写我们的树：

\[/a/b/c \mapsto a(b(c))\]
\[/a/b/c+d \mapsto a(b(c, d))\]

接着注意到统一可作为匹配和分解树的一种自然的算法，基于统一的匹配和分解为查询提供了基础。

根据这个讨论，我们来看看π演算中的I/O行为：

input: x?(a(b(X,Y)))P ↦ for(a(b(X,Y)) <- x)P
output: x!(a(b(c,d)))

当这些被置于并发执行中，我们有

for(a(b(X,Y)) <- x)P | x!(a(b(c,d)))

它被求解为 P{ X := c, Y := d }，也就是说，我们在某个环境中开始执行 P，在该环境中 X 被绑定为 c ， Y 被绑定为 d 。我们用符号写下求解过程:

for(a(b(X,Y)) <- x)P | x!(a(b(c,d))) → P{ X := c, Y := d }

这引起了一个非常自然的解释：

  • 输出将资源置于对应位置：
x!(a(b(c,d)))
  • 输入查询在位置上的资源
for(a(b(X,Y)) <- x)P

这只是故事的开始。通过反射，我们允许信道的名称自身也是结构，比如上面例子中的x。这允许我们通过命名空间来细分存储资源的空间。命名空间是从安全到分片的各种特性的基础。

RChain智能合约模型

现在我们对RChain智能合约模型已经有一个完整的描述。它编纂在rholang的设计中。它从反射所得到的特性数量，从宏到协议适配器，足以值得引起重视。然而，退一步说，我们将看到

  • 它有一个健全和正确的类型系统
  • 一份形式化规范
  • 将形式化规范渲染为能工作的代码
  • 它决定了一份构建时正确的虚拟机的形式化规范
  • 这决定了一个清晰的编译策略，一系列构建时正确的到虚拟机字节码的转换规则，该虚拟机已经被现场测试了达20年之久。

现在，以这个出发点和以太坊中Solidity和EVM的当前状态做比较。如果目的是产生一个可信的时间线，通过它我们可以得到一个区块链节点网络，在其上面运行形式验证、构建时正确的代码，那么与以太坊网络相比，这种方法也有明显的优势。显然，有足够的市场兴趣来支持这两种选项的发展。

[SM15]Mike Stay and Lucius Gregory Meredith. Higher category models of the pi-calculus. CoRR, 2015. URL: http://arxiv.org/abs/1504.04311.