本文译者：币友_Anthony，首发于巴比特资讯

原文地址：https://www.researchgate.net/publication/344501038_Smart_Contract_Languages_A_Thorough_Comparison

年中时， IOSG博文有提到过，将会在形式化验证(Formal Verification)方向做一些布局。形式化验证是什么？

而前不久，Algorand发布的 smart contract language 不是图灵完备的。智能合约开发语言图灵完备重不重要？

突然，我发现不仅要对Solidity智能合约开发语言里函数有所了解，更需要了解整个智能合约开发语言生态全景。

本文就智能合约语言作一个比较，除了Solidity外，还有很多其它不为我们所熟知的智能合约语言 如Vyper、Mandala和Obsidian等在不同方向改善智能合约的编写。

然而，就像我们通常只记得第一名一样，目前开发者主要也是集中于使用Solidity进行开发，虽然可能不会是最好的.

智能合约语言，还是一个很早阶段，未来会是一个什么样的情况呢？值得我们畅想。

智能合约语言：一个彻底的比较

近年来，智能合约的发展越来越受欢迎。然而，这导致它成了恶意势力的新攻击对象。最近对智能合约的一些攻击已造成数千万美元的损失。由于智能合约本质上是不可变的，因此需要考虑新的方法来缓解这些攻击。检测软件缺陷的一种方法是使用静态代码分析工具。另一种方法是开发新的智能合约特定编程语言，通过设计，抑制已部署代码中某些类别的漏洞。像Solidity和Vyper这样的流行的智能合约语言正在迅速发展，但是研究人员也在用一些不太知名的语言来寻找新奇的改善灵感。

本文，我们将探讨智能合约语言设计的现状，并比较这些语言及其对智能合约发展的适用性。将特别关注这些语言如何解决智能合约开发中固有的安全问题。

一、 简介

智能合约的想法从上世纪90年代就已经出现了，但直到2009年区块链的出现，它们才得以实现。智能合约可以在不信任的环境中执行可信任的代码。这意味着参与者（用户、计算机应用程序和其他智能合约）可以确保智能合约已经执行，结果是合约执行情况的准确表示，而无需信任执行者或智能合约开发者。这完全是通过在分布式去中心化、全局和透明的区块链上托管智能合约来实现的。这种新的开发环境支持一种全新的应用程序，即去中心化应用程序（dApp），但给智能合约的开发者带来了一系列新的挑战。

因为智能合约部署在区块链上，所以每个人都可以查看它们的源代码。区块链也是不可变的，智能合约的含义是，一旦智能合约被部署，就不能在更改。开发人员必须确保他们正在部署的代码是正确的并且没有bug。因此，需要新的语言来满足这种新环境的具体需求。智能合约中的漏洞可能代价高昂，不仅是在安全漏洞方面，而且在实际资金方面也是如此，因为智能合约通常管理加密货币的持有和分发。

本文的其余部分安排如下：在第二节中，我们将介绍智能合约的背景和一些安全问题，在第三节中我们将讨论相关的工作，在第四节中我们将回顾当前的智能合约开发语言，在第五节中我们将讨论和比较这些语言，在第六节我们总结。

二、背景

智能合约的概念最早由Nick Szabo在1996年提出[1]。直到2015年开发以太坊平台，开发真正的智能合约才变得可行。智能合约是一种自动执行的计算机应用程序，它执行合约时不需要来自第三方的验证。这意味着交易双方不需要相互信任就能进行交易。

以太坊是最受欢迎的智能合约平台[2]。它提供了一个称为以太坊虚拟机（EVM）的执行环境，它是一种基于堆栈的、图灵完备的语言。它类似于汇编，为离散操作提供操作码。因为它是图灵完备停止问题适用和执行可以永远运行。为了防止这种情况，为了执行智能合约，调用者向矿工支付费用。这被称为气体，以以太坊网络的货币支付，称为以太（ETH）。每笔交易都有一个最大的天然气成本。因此，如果一个事务试图执行比gas所允许的更多的操作，则抛出异常并回滚事务。

智能合约容易受到传统软件部署不易受到的特定安全漏洞类别的攻击。其中包括重入、锁定以太、未处理的异常和事务顺序依赖[3]。以太坊网络上最臭名昭著的安全漏洞之一是利用名为TheDAO的智能合约的重入漏洞[4]。攻击者使用另一个智能合约对DAO智能合约进行递归调用，捐失金额为5000万美元的ETH。

研究人员开发了多种方法来减轻这些漏洞。一种方法是使用静态分析工具，如Oyente[5]，在编译字节码之后对其进行分析，以确定它是否包含任何缺陷。Perez等人回顾了分析智能合约的现有工具，发现这些工具检测特定漏洞的能力存在较低的重叠率[3]。例如，在分析774份合同中的重入缺陷时，Oyente和Securify[6]（另一个静态分析工具）只有23.9%的合约重叠。在实践中，这意味着开发人员将无法依赖单一工具来一致地发现其应用程序中的漏洞实例。

另一种方法是开发新的智能合约语言，使编写具有已知漏洞的代码变得困难或不可能。除了solidity，还有其他智能合约编程语言，其中包括 Vyper[7]、Mandala[8]和Obsidian[9]。每种语言都采用不同的方法来改进现有的工具。在本文的其余部分，我们将分析智能合约语言，并比较它们减轻漏洞的方法。

三、 相关工作

Parizi等人[10]分析和比较三种不同区块链的三种不同语言。它们包括以太坊的Solidity，Kadena区块链的Pact，以及Tezos区块链的Liquidity。然后，他们进行了一个实验，招募开发人员学习这些语言，并实施了三个智能合约，以确定这些语言在新开发人员的可用性方面如何叠加。Solidity被认为是最容易学习的语言。另一方面，他们在以Pact和Liquidity编写的智能合约中没有发现已知的安全漏洞，而在以Solidity编写的智能合约中却发现了重入和拒绝服务漏洞。

Harz和Knottenbelt[11]研究智能合约语言和形式化验证方法。它们考虑每种语言的范式、语义、安全关注点、指令集和度量属性。他们还回顾了其中一些语言的形式化验证工具，并描述了这些工具如何很好地检测智能合约中的漏洞。他们指出，语言的设计会对验证工具的有效性产生影响。

Jansen等人 问了一个问题，智能合约语言是否需要图灵完备。他们分析了以太坊区块链上部署的智能合约，发现只有35.3%的合约使用while循环、for循环或递归。他们的结论是，非图灵完备语言对于智能合约开发的大多数场景都是有效的。

四、 智能合约语言

智能合约语言的开发仍处于早期研究阶段。少数语言已经很少被使用了。其他的，如Mandala[8]和Obsidian[9]，仍处于概念化和实现阶段。在这项研究中，我们考虑了可以被视为死亡了的语言、正在被开发的语言和正在被创造的语言。表中我展示了这里考虑的所有语言和一些相关的细节。

A、 Solidity

Solidity[14]是大多数开发人员在以太坊网络上创建智能合约时的默认语言。它是为编写智能合约而设计的。图1显示了2016年1月至2020年1月期间使用Solidity和Vyper on Stack Overflow标签的问题数量。此处讨论的其他语言的标记未显示在搜索结果中。

它的主要结构是合约，它是面向对象语言中类的分析。Solidity合约具有可见性modifiers的函数，可以通过网络将值返回给调用者。Solidity的一个新特性是modifiers，它本质上是一个封装另一个函数的函数，但通过将modifiers名称添加到函数签名中来调用。虽然在很多情况下都很有用，但是这个特性混淆了开发人员的意图，并且常常被忽略。由于以太坊上的智能合约无法调试以遵循其执行流程，因此尽可能明确地设置函数非常重要。图2示出了简单钱包合约的实现以及称为onlyOwner的modifiers的使用，其目的是将公共功能限制为合约的所有者。可以看出，modifiers就像函数签名本身的语言级关键字一样使用。开发人员很容易忽略是否对函数应用了modifiers，这会导致错误的安全感。此外，它混淆了代码执行流程。

B、 Vyper

以太坊网络上第二种最流行的语言是Vyper[7]，它是一种智能合约语言，其语法受Python启发。它避免了图灵的完备性，禁止在数据结构上循环，并且不允许递归。循环仍然是允许的，但前提是迭代计数可以在编译时确定。它使用注释来修改以太坊虚拟机的功能可见性和特性，例如应付款。

图3显示了Vyper中的一个示例合约。合约是一个简单的银行。它接受存款，并允许来电者一次取款。这里需要注意的是@nonreprent注释。在同一个函数中调用另一个函数的锁。如果没有这样的功能，调用者可以在同一事务中重新输入此函数，并在调用者余额设置为零之前提取该合同的所有资金。

C. Obsidian

Obsidian[9]，[15]是一种与区块链无关的编程语言。它用类型引入状态信息，称为Typestate。所有对象引用可以是拥有的，也可以是无主的。一个对象只能有一个拥有的引用，但可以有多个无主引用。实际上，这意味着在给定的事务期间只有一个调用函数可以改变对象的状态。Obsidian的另一个新特点是它的客体状态机制。对象的每个状态定义都可以定义一组字段，这些字段只有在对象处于给定状态时才有效。

图4显示了用Obsidian编写的智能合约示例。使用存款功能，来电者将钱存入钱包，钱包的状态从空转满。当调用方退出时，首先需要获得对货币的引用，因为一旦状态转换回空，字段货币就不再可用。

D、 Flint

Flint[16]不再处于积极开发阶段，但它为智能合约专用编程语言的开发引入了一些新颖的思想。这三个关键思想是：

1） 调用者功能。每个公共函数必须包含外部调用方可以访问此函数的声明。此外，编译器将分析这些函数以查找对内部函数的引用，以确保调用方可以访问内部函数。
2） 资产。这些是特殊类型，例如Ether，不能被复制、销毁或错误地创建。
3） 限制写入状态。每个对智能合约的内部状态进行变异的函数都必须显式地使用mutating关键字进行注释。

在图5中，有一个用Flint编写的智能合约示例。声明智能合约有多个步骤。首先是合约的定义和字段的声明。接下来声明函数。它们按调用方功能分组。如图所示，存款和取款功能只能由已经在资金图中的调用者访问。

E、 LLL

LLL（Low level Lisp like Language）是以太坊虚拟机的汇编程序之后开发的第一种语言[17]，它只是围绕着汇编程序本身的一个薄薄的包装器。它有一个受Lisp启发的语法，每个智能合约都是一个s表达式。它提供对执行环境内存的直接访问，并且可以针对速度和更小的二进制大小进行优化。它是图灵完备的，允许程序员访问EVM中可用的任何功能。

F、 Bamboo

Bamboo[18]是一种面向以太坊虚拟机的智能合约语言。它的语法有点类似于Solidity的语法，并且支持所有相同的默认类型。该语言的目标是显式地建模状态转换。函数返回时必须显式声明当前协定的状态。状态被建模为具有一组离散函数的多个合约，这些函数仅在合约处于给定状态时可用。

图7中的列表展示了另一个示例钱包智能合约。有三种状态：钱包，空墙，满墙。钱包状态是在合约部署期间执行的初始状态。如果我们需要更多的初始化，我们将在默认块中进行初始化，而不是立即将合约转换为空wallet状态。在合约中，它有一个映射状态的访问权。调用方将资金存入钱包后，它将转换为FullWallet状态，现在只能调用取款函数。

G、 Mandala

Mandala[8]是一种在研究发展阶段提出的语言。它的定义特征是使用代数数据类型。这些类型有多个构造函数，每个构造函数都有多个字段。它支持Java等泛型类型。该语言的主要设计目标是安全性和可审计性，因此它不是图灵完备的，不允许在编译时上线未知的循环。

图8显示了另一个钱包示例。每个Mandala智能合约由多个模块组成，这些模块限制功能和对状态的访问，这与Bamboo使用契约管理状态的方式非常相似。在这种情况下，合同很简单，没有必要。Drop关键字意味着任何调用方都可以删除此值而不使用它，Persist关键字表示可以持久化该值。类型也被参数化，因此可以想象出多种钱包类型，例如Wallet[Eth]、Wallet[Btc]。在取款功能中，金额值是通过参数分解从钱包对象中提取出来的，而不是直接引用。

五、 讨论

目前，Solidity是开发新型智能合约项目的最佳选择。它提供了一个强大的工具、文档和示例生态系统。许多智能合约和去中心化的应用程序都是用Solidity构建的，并部署了以太坊区块链，每天处理大量交易。它正在积极的开发中，语言设计者正在添加新的功能，迫使开发人员明确他们的意图，避免简单的错误。

第二个不错的选择是Vyper，但它远不及文档和开发人员工具那样可靠。尽管如此，它的设计更注重安全性，并提供了很好的保护措施来防止容易被利用的漏洞。它类似于Python的语法使许多开发人员熟悉它。

这里讨论的其他语言还不够成熟或开发不够活跃，不足以在新的开发项目中认真考虑。LLL实际上是由Ethereum基金会使用的一些早期智能合同，但是它的语法和对低级别内存管理的要求使得它很难重新命名。Mandala还没有编译器。虽然它显示了安全管理状态的希望，但它处理类型的方式与已建立的语言大不相同，因此呈现出陡峭的学习曲线。Bamboo有一种管理状态的新方法，它迫使开发人员明确意识到在智能合约的整个生命周期中，哪些功能和应用程序状态是可用的。然而，这个项目已经两年没有新的提交了，并且缺少编译器之外的任何工具。Flint是一种死气沉沉的语言，除了最初描述其设计的研究论文外，我们无法找到任何信息。因此，尽管它引入了许多有助于编写更安全的智能合约的功能，但对于开发来说，这是一个不可能的选择。Obsidian仍处于早期发展阶段。它显示了它的前景，因为它专注于开发人员的人机工程学和安全性，但是它的所有权概念加上TypeState，使得开发人员可以一下子记住很多可移动的部分。

六、 结论

目前，智能合约开发语言的前景相对较小，但对新方法的研究很多，现有的语言也在频繁地变化。当前寻求图灵完备并提供面向对象特性的语言，虽然功能强大，但已经表明用它们编写的智能合约容易受到严重错误的影响。将一种语言的特性限制到不再图灵完备的程度，这种方法有助于消除某些类的错误，但要求开发人员以根本不同的方式编写代码，而不需要使用循环或递归。令人惊讶的是，最适合智能合约编程的函数式编程范式只有两种死的语言来表示。由于一个可利用的bug的成本如此之高，因此需要对智能合约编程语言的开发进行更多的研究，这种语言限制了副作用，并且仍然具有良好的开发人员工效学。