本月初我们发布了区块链编程语言Simplicity的源代码。
Simplicity旨在解决在区块链环境下编写复杂的智能合约时遇到的一系列问题。在Simplicity诞生之前,区块链编程语言通常要在表达能力和可靠性之间作取舍,开发者要么开发一个复杂但不可靠的智能合约,要么只能开发一个可靠单功能简单的智能合约。有了Simplicity编程语言,开发者终于可以开发复杂又可靠的智能合约了。
Simplicity编程语言与Blockstream的Elements平台相互兼容,在Elements上开发侧链或独立区块链的开发者们很快就能使用Simplicity带来的新功能了。由于Liquid也是基于Elements安装的,Liquid网络也会支持Simplicity,Liquid用户将有机会使用许多有趣的应用,比如几乎无需信任的第三方托管、金库以及其他更复杂的智能合约。
本月发布的源代码包含:
- Coq中正式指定的核心Simplicity语言及其扩展的指称语义。
- Coq中正式指定的核心Simplicity语言的操作语义。
- 使用Haskell编写的Simplicity语言的解释器,类型检查器和序列化。
- Simplicity表达式参考示例,包括加密操作,如SHA-256和EC-Schnorr签名验证。
- 关于Simplicity语言的详细技术报告。
为什么选择Simplicity?
区块链带来了许多传统编程语言无法解决的独特的问题。
- 所有用户都必须同意所有环境中的计算结果。
- 智能合约中的每一位参与者都必须了解所有可能的预先输入项目的结果。
- 所有用户必须能够阻止会消耗过多内存或计算时间的拒绝服务攻击。
- 智能合约中的每个参与者必须能够预先了解所有可能输入的程序执行成本。
现有的为区块链而设计的编程语言,如以太坊的EVM,仍然不能解决这些问题。就在最近,EVM的一次升级在测试中失败了,因为安装并未就计算结果达成一致。智能合约逻辑错误以及项目超过可用资源导致资金被盗或者无法找回。
另外一方面,比特币的脚本语言只有数字签名检查、时间锁和哈希锁这几种组合。尽管比特币脚本语言如此原始而简单,开发者们还是在此基础之上开发了像闪电网络这样优秀的协议;尽管如此,在面对复杂的智能合约时,比特币脚本语言表达能力还是稍显不足。
Simplicity的灵活性和强大的表达能力将使得开发者能够进行任何所需要的计算,同时也能验证智能合约的安全性和成本。
Simplicity是什么?
Simplicity是一种面向基于区块链的智能合约的低级编程语言和机器模型,设计的初衷就是让它拥有简单的语义,可以通过形式化方法进行静态分析和推理。 Simplicity语言由其在Coq证明助手中的安装来定义。
Simplicity的核心语言十分简单,甚至可以将之全部印在一件T恤上,然而这门编程语言简单并不意味着它的开发过程简单,这是因为:
- 区块链要求的编程模型与普通的编程从根本上就不同。区块链的任务是验证计算结果,而不是要进行计算。这个区别十分微妙,但却会造成天壤之别,因为即使没有图灵完备性也能够验证任意代码执行。
- 智能合约上线后就无法更改了,即使有错误也无法更正。Simplicity使得用户能够为他们的智能合约创建正式的正确性证明,从而解决了这个问题。
- Simplicity是可直接执行的低级语言,更接近于汇编语言而不是Java或Python。我们希望用户能够用一种或多种更高级别的语言编写智能合约,然后将其编译为Simplicity。
Simplicity有哪些新功能?
自上一次发表关于Simplicity的博文以来,我们一直在努力从实验语言研究转向更正式的语言规范。
我们在Coq证明助手中重新安装了Simplicity语言:
- 我们具有完整Simplicity语言的指称语义,包括支持见证数据、断言和委派的语言扩展。
- 基于免费类别的名为“Bit Machine”的抽象机器的正式规范为核心Simplicity语言提供了操作语义。
- 以无标记最终样式开发的Haskell装置允许用户尝试评估、执行和类型检查Simplicity表达式。
- Simplicity语言扩展的模块化允许用户在不使用语言扩展时忽略语言扩展的影响。
- 我们有许多用于加密原语的Simplicity表达式,包括我们在Simplicity中重新安装libsecp256k1。
- 技术报告将提供Simplicity语言的非正式数学规范,并提供Coq和Haskell开发的指南。
虽然Simplicity开发仍在进行中,但开发者现在已经可以自己探索Simplicity语言了,因此是时候将Simplicity的开发开放给公众并创建邮件订阅名单了。
下一步将迈向何处
Simplicity接下来的开发任务将会多头分工进行。
我们负责的开发任务包括:
- 完成C翻译器。
- 为各种常见的加密功能实现喷气式库。
- 使用可验证的C证明我们的C解释器和喷气机是正确的。
- 将Simplicity集成到Elements区块链平台中。
其他的开发任务包括:
- 开发Simplicity代码优化器。
- 创建新的或改造现有的高级智能合约平台,例如Ivy,来生产Simplicity。
- 将Simplicity加密原语的功能正确性与加密协议的正式正确性相结合,以构建经过全面验证的智能合约。
期待你加入我们的项目。
原文链接:https://blockstream.com/2018/11/28/simplicity-github/