Anoma 基础知识

Anoma 在 Elixir 中

本文解释了为什么 Anoma 使用 Elixir 编程语言构建。

摘要

本文解释了为什么 Anoma 使用 Elixir 编程语言构建:

  • Elixir 允许开发者在系统运行时检查系统,并更新其运行代码而无需重启。
  • Elixir 编译成 Erlang,一种成熟的编程系统,专为构建具有"让程序崩溃"哲学的健壮、容错的网络系统而设计。
  • Elixir 的"代理模型"与 Anoma 的架构之间存在天然的契合点,Anoma 的架构基于消息传递的"引擎"。
  • 由于语言结构与系统设计相匹配,实现复杂度降低。
  • 上述特性简化了形式化验证工作。

因此 Elixir 提供了合适的抽象层次来根据其规范构建 Anoma,同时保证了良好的开发者体验并承诺支持未来的验证。

Anoma:为什么选择 Elixir?

Anoma 是一个具有异构信任的去中心化操作系统。它具有以下特性:

  • 它必须支持一个由交互参与者组成的庞大网络。
  • 它必须具有鲁棒性。
  • 它的核心组件是"引擎"

Elixir,因此,似乎适合我们的实现。

  • 它的交互式环境支持生产开发实践和多智能体系统分析。
  • OTP 基础促进了应用的健壮性。
  • 引擎和 GenServers 之间存在关联。

让我们解释这些要点:

实时交互系统

在构建任何系统时,开发者需要两个核心功能:

1. 了解系统是如何运行的。

2. 确定在设计执行过程中是否存在失误。

对于大多数软件项目,这意味着相应地:

1. 抽象地思考代码 (...这可能耗时)。

2. 追踪系统执行 (...这可能难以理解)。

幸运的是,Elixir 建立在 Erlang/OTP 的基础之上。从实际角度来看,这意味着我们可以获得一个实时交互环境来询问有关我们系统的问题。它赋予我们的具体功能是:

#### 热代码重新加载

这意味着我们可以在本地运行软件,并且能够更改它的任何部分,而无需关闭和重新启动服务。这对于尝试新想法来说是无价的!

#### 底层环境反射

底层反射为系统提供了它需要的信息,以便能够反馈。如果没有对系统的访问权限,交互式系统将很快变得不透明!

#### 整个系统从用户外壳可用(从解析器到编译器,到可视化套件)

这使得熟练的工程师能够诊断问题,并看到他们所做事情的实际影响。这是与让人类能够调试一亿英里外太空探测器的相同的技术的一部分!

#### 系统与语言之间缺乏人为的区分

这意味着系统的核心功能是通过语言本身实现的,证明其足以构建一个高度稳健的系统。

我们不必只是坐下来思考实现组件如何组合在一起的架构,这些工具允许我们向底层系统提问:"请给我们 Anoma 流程的布局":

*[图示:系统进程布局]*

图示的具体细节并不重要。重要的是系统能够自我反思,这有助于解释我们正在构建的整个系统。也就是说,实现过程可以与构建者进行对话,围绕自身塑造讨论。例如,如果我们对图示中的某个节点感到好奇,我们能从中获取哪些信息呢?

*[图示:节点诊断信息]*

我们可以看到,现在我们有了关于特定节点的诊断信息,包括其状态堆栈跟踪等。

有了这些属性和功能,这使得 Elixir 与常用语言(Java、Rust、Python 等)有很大不同。

既然如此,存在一些语言类型表现出相同的特点,其中一些拥有更优越的可视化技术。是什么让 Erlang/OTP 系统与它们相比显得特别?

设计健壮的系统

要理解 Elixir 的特殊之处,我们首先必须回到 Erlang 和 Beam 旨在解决的问题。Joe Armstrong 的论文:在软件错误存在的情况下构建可靠的分布式系统,阐述了它们的问题领域:

  • 系统必须处理大量的并发活动
  • 动作必须在某个时间点或一定时间内执行。
  • 系统可能分布在多台计算机上。
  • 系统用于控制硬件。
  • 软件系统非常庞大。
  • 系统展现出如功能交互等复杂功能。
  • 系统应能连续运行多年。
  • 软件维护应在不停机的情况下进行。
  • 存在严格的质量和可靠性要求
  • 必须提供对硬件故障和软件错误的容错能力。

为了解决这些问题,他创建了一种理念和需求,即底层操作系统和语言应该具备,从而创建了 Erlang/OTP。

为了展示系统拥有的功能样本:

#### 系统具有非常廉价的进程

```elixir

iex(mariari@Gensokyo)10> :timer.tc(fn -> spawn(fn -> nil end) end)

{10, #PID<0.1689.0>}

```

这段代码展示了一个进程仅需10微秒即可生成!

#### 应用程序的架构被划分为一系列进程,每个进程通常被称为演员

演员是很有趣的对象,因为它们具有以下核心特性:

  • 它们包含一些它们维护的状态
  • 它们可以发送和接收消息
  • 消息在相同的两个演员之间顺序处理(顺序是保证的)!

#### 进程是隔离的

这意味着如果一个进程崩溃,它不会影响其他进程。Erlang 电影很好地展示了它们在真实系统中的实际应用!

#### 进程由一系列监督者管理

监督者的有趣之处在于它们负责许多进程。当它们所监督的进程崩溃时,它们有关于其控制下其他进程将发生什么的政策。

人们意识到,仅靠演员本身不足以构建一个健壮的系统,而这正是大多数其他演员模型所缺少的关键组件。

#### 其理念是"让它在崩溃"

使用监督者,这是一种创建可靠和健壮系统的非常有效的策略。

当崩溃发生在早期时,我们可以隔离错误,但在使用 Either/Result/Maybe 类型时,这样做很困难,因为这些策略往往会丢失堆栈信息。此时,监督者可以重启崩溃的组件,帮助系统恢复正常行为。

此外,由于系统部分宕机可能是正常现象,通常需要设计一个稳健的监控系统,使系统能够优雅地降级。一个常见的例子是拥有一个功能完备的系统,但在某些外部服务宕机时(比如查询外部服务获取图像或 AI 响应),我们可以切换到更简单的行为,直到问题解决。

这也有助于应对底层硬件错误的情况,比如当高完整性组件因宇宙射线导致位翻转时,应用程序不会崩溃停止,而是可以崩溃并执行合理的重启行为。

#### 系统具有公平的并发性,拥有自己的调度系统

这意味着您的进程不会因资源不足而受限。

这只是使 Erlang/OTP 系统在众多交互式系统中脱颖而出的功能之一。对于大规模的交互式代理系统,鲁棒性至关重要。

然而,Elixir 是否有助于满足 Anoma 的特定需求?如何实现?要回答这个问题,我们必须参考规范

实现引擎

Anoma 是一个理念,具体体现在一个协议规范中。它是实现应该遵循的真理来源。它的主要价值在于作为一个吸引人的理念模型,这将驱动用户与代码库进行交互。

因此,实施过程必须尽可能清晰、自然地符合规范,这是至关重要的。用户所寻求的是呈现方案中具有所需特性的实例。也就是说,他们需要确信存储库中某段代码确实是所描述系统的实际实现。

为了让这个过程变得简单,工程师们需要有一个良好的界面,使得在规范的核心概念和我们的代码之间建立连接尽可能简单。

例如,如果你对函数感兴趣,呈现 `id : Bool -> Bool` 作为 `lambda x -> x` 或 `{{true, true}, {false, false}}` 是否重要。数学中我们并非处处使用集合论是有原因的。如果你将函数视为输入并输出东西的东西,类型理论方法可能更容易理解和处理。

遵循这个想法,所需语言的一个良好要求是有一个对应核心概念的一流公民该规范的:the 引擎。Anoma 基础设施中的几乎每种功能都以特定引擎的功能形式进行规范。例如,Mempool 行为通过 Mempool 引擎实现;交易执行通过执行引擎实现。

一个引擎具有多个属性,其中包括:

  • 它是状态化的
  • 它可以接收消息
  • 它可以发送消息
  • 消息是按顺序处理的

那么引擎是什么?看起来像是一个代理,对吧!现在哪些系统将代理视为一等公民?从上一节我们知道,基于 Erlang 的系统就是这样做的!

拥有一个良好的语言行为模型不仅能够简化代码库的理解,还能提高来自规范方面的对 Anoma 开发感兴趣方的参与度,同时也能为未来进行的内部验证和审计工作提供可信度。

Anoma 所进行的正式验证工作并非针对特定实现的验证:实现方式可能存在差异,规范实现也可能因时间选择而变化。相反,系统属性的证明将通过 Anoma 规范的正式化来完成。众所周知,证明的有效性取决于系统初始正式化的质量。规范和实现的基础概念越接近,我们关于 Anoma 的证明就越有可能与关于我们的 Elixir 实现的证明相吻合。

结论

我们选择 Elixir 来开发 Anoma 节点软件。Anoma 节点由多个独立运行的组件组成,这些组件需要被协调和连接(例如,交易执行、节点内部通信、配置等)。从开发者的角度来看,能够实时地内省这些独立组件、更新它们并操作它们是有益的。此外,Erlang 虚拟机为我们提供了构建和以稳健、可扩展的方式连接此类独立进程系统的基础构件。

Anoma 的规范规定,任何节点由不同的"引擎"组成,这些引擎是隔离的进程,各自负责处理 Anoma 节点的一部分职责。Erlang 虚拟机及其计算模型中的进程与共享无内存映射几乎 1:1 对应于 Anoma 规范中提出的架构。这意味着,与其它计算模型相比,该规范的实现将具有更低的偶然复杂性。

因此,选择使用 Erlang 虚拟机来实现 Anoma 规范,为我们提供了更好的开发者体验,并减少了 Anoma 规范与其物理实现之间的阻抗不匹配。