再好的程序员也管理不好资源
近10年来由于安全事件导致的加密资产损失高达35.8亿美元，而有60%的漏洞是因为资源（内存，线程，文件）管理不当造成的，无论你是最顶级的开发者，还是你用了最先进的开发方法，都无法避免这个情况。
事实证明程序员根本管理不好资源，做再多的检查，写再多的测试还是避免不了内存泄露，忘记释放文件句柄。
之前的智能合约对信息和资源没有区分，这是导致问题的关键。采用值（value）的方式记账的话，值是一种信息，信息可以被随意复制，这就很容易出错。正常的转账流程是Alice给Bob转账，系统会先扣掉Alice的钱（减去value），然后给Bob加上一定的钱（加value），进而完成一次转账交易。但是如果转账失败，可能会导致Alice的钱变少了，而Bob的钱没有增加。
资源，资源，还是资源
Move语言采用了传统理论”线性逻辑“的类型，叫做资源类型。这样数字资产就会被定义为资源类型，就会有和资源类型一样的特点：
- 不能被复制
- 不能凭空消失（上面的Alice转账失败的例子）
这个特性对去中心化金融非常关键，可以解决很多问题：
- 钱不应该转但是转了
- 一份钱转出了很多份
- 系统的内容没有合理的释放
资源是一等公民
函数编程中，函数可以赋值给一个变量，可以当做参数传递给另外一个函数，也可以从一个函数当做返回值返回。这时候函数和数据也没什么区别，所以我们叫它“一等公民（First-class Citizen）”。
资源是一等公民，指的是，数字资产作为资源可以赋值给一个变量，可以当做参数传递给另外一个函数，也可以从一个函数当做返回值返回。
这样在编程语言层面对资源的支持极大地降低程序员管理资源的难度。
但是对编程者来说需要学习全新的资源使用方式，有一定门槛。
系统类型和形式化验证
move是一种对形式化验证特别友好的语言，甚至为此牺牲了语言的特性。因为在move中不支持动态指派（dynamic dispatch），动态指派是一种可以指定在运行时才决定调用哪个函数的方式，如很多编程语言中的动态继承机制，智能合约solidity中的delegatecall也是一种动态指派。在move中所有的合约路径都在编译期就可以确定，可以充分的进行分析和验证。
类型系统以及支持类型的虚拟机是一个非常好的工程折中。
形式化验证的重要性
Java标准库的一个排序中被发现有一个漏洞，而这个库每年会被调用几千万次。有形式化验证就可以发现这些bug。
以太坊就有很大的历史局限性，未来的语言设计，线性逻辑和类型系统会是首先考虑的。
技术上，区块链可能会引领互联网的发展。
总结
- 智能合约需要比以往更强大的编程语言理论的支持，使得智能合约编程语言设计的难度大大提高，比如类型系统，线性逻辑，虚拟机设计等等
- 线性逻辑，类型系统将成为未来这个领域的标准配置
- 在语言设计之初就要考虑形式化验证的可行性
- 随着move语言的发展，包括线性逻辑在内的一些特性将在其它编程语言中得到更广泛的应用
- move是为了智能合约语言设计的区块链
网友评论