来源：金融界网站
作者：曹静
年8月21日，火币集团CTO程显峰在火星财经主办的“POWER全球开发者大会”发表演讲。
以下内容为编辑整理所得：
最牛程序员都做不好的资源管理交给线性逻辑
计算机系统的漏洞大多都是资源管理不当造成的。之前经常遇到一些团队，总认为自己家的程序员能管理好，但其实只要开发规模足够大，程序员就不可能做好资源管理。
内存泄露，可以通过程序员的不懈努力，或系统性方法避免吗？答案是不能。
公开数据显示，微软最近12年所有的系统漏洞中，60％都是因为内存泄露。事实证明，全世界最顶级的程序员都做不好资源管理。在银行系统中，这类问题就更多了。
Move语言是Facebook开发的全新编程语言，它带来的最重要的变化就是线性逻辑，因为线性逻辑可以保证“资源只能且必须被使用一次”。
线性逻辑并不是新概念，早在80、90年代就已经有很多人在讨论。现在，线性逻辑被引入Move语言，是革命性的。
资源和智能合约有什么关系？
首先，要先区分资源和信息。举个例子：“表示感谢”是一种信息，A对B表达感谢，并不妨碍A感谢其他人，因为信息可以被复制的。但资源不行，比如内存、文件句柄就是有“独占性”的资源。而之前的传统计算机语言对信息、资源并没有正确区分，这就是很多问题的关键。
在这样的思考框架下，钱、资本就是资源。
转账等智能合约的关键引用非常重要。仔细思考一下，智能合约的关键漏洞无非就是该转的钱没转、钱消失了，要么就是不该转的钱凭空出来了。如果有一个体系，可以从根本上管理好智能合约的资源，那可靠性、安全性会提高不止一个量级。
线性逻辑就可以解决这种问题，但“资源被使用一次”并不容易实现。
未来线性逻辑或许是你我的“救命稻草”
计算机系统里有一个典型的难题，信息传递至少一次或至多一次是比较容易的，但“刚好一次”很难。到底什么可以“只做一次”正确的转账？什么又能证明你设计的智能合约确实能完成这样的目标？这些都是很难回答的问题，但对庞大的智能合约承载的金融体系却又至关重要。
线性逻辑除了可用于内存分配、管理文件句柄，在资源管理方面的应用也已经被证实，是非常有效的。如果把钱看作资源，那线性逻辑就是这类问题的答案。
智能合约需要大量的人工审查，可靠性、应用范围都严重受到限制，制约了智能合约未来的发展。而线性逻辑编程语言，可以通过编译器检查资源是否存在泄露。
以太坊智能合约出来以后，大家开玩笑说：“以后的律师都得会读智能合约了。律师的合约一般是文本，以后就要变成智能合约，或许新的法律体系都会建立在智能合约里。看不懂代码，做不了肉眼静态检查，那大家都不用干了。”但如果使用线性逻辑，编译器就就可以极大程度上降低人参与的难度。程显峰表示，这就是线性逻辑对推动智能合约广泛应用的价值。
为了发展更好，请对形式化验证友好！
Move非常重视类型系统，和支持类型系统的虚拟机。与已知的大部分虚拟机不同的是，Facebook在非常有远见，在开放系统重新设计了语言。
除此以外，Move语言还减弱了动态分配方面的考虑，这可以算是语言特性的一种牺牲，但是它对形式化验证的处理非常友好。这是Move语言在设计上非常好的折中。
说起形式化验证，很多人都觉得是小题大做。举个非常惨烈的例子：在面试程序员的时候，一般都会考算法题。面试官会让程序员写一个排序算法，这是最入门、基础的东西，不可能有人不会。但世界最顶级的程序员，比如Java标准库的程序员，突然有一天发现他的排序算法有漏洞，而且这个漏洞非常隐秘，以至于发现以后很多年都修不好。这就是荷兰团队在标准库里发现的漏洞，一个每天被用数以亿计次的漏洞。
事实就这样的，不是我们认为会写就能写对，智能合约也不是能完全按照设想实现的。如果没有形式化验证，某些问题可能一辈子都找不到原因。这种漏洞在智能合约中被发现，那就是灾难级的。所以对形式化验证友好，对编程语言未来的发展非常重要。
随着Move语言的发展，它的许多特性会不断被其他语言吸收，得到更广泛的应用。在技术创新上，区块链行业已经引领了现在普通互联网，反过来互联网会不断吸收，然后推动自己的发展。
程显峰和大众观点不太相同的地方是，他认为Facebook先做了Move语言，后来才有了Libra，而不是Facebook特意为Libra设计的Move。理由是，Libra所有的设计都是围绕Move进行的，而且白皮书里提到的，对区块链的抽象理解，跟以前的观点完全不同。
最后，智能合约需要比以往更强大的编程语言理论的支持。线性逻辑和类型系统未来将成为这个领域的标准配置，这两件事是智能语言最优先考虑且不可或缺的特性。如果想做智能合约，你必须要了解。
