时艳强对话胡凯：智能合约距离智能还有多远

本期速览：北航计算机学院的胡凯教授在分布式计算、智能合约以及形式化验证方面有很深入的研究，发表了50余篇SCI/EI相关的论文，与胡建平先生主编了目前国内最权威的分布式计算方面的国家级教材《分布式计算系统导论》。

胡凯教授做客布洛克科技时点对话，给大家关于区块链与智能合约做了一期精彩分享。胡教授长期对分布式计算理论和技术开展研究，他讲到，2000年以来分布式计算技术有很多巨大的进步，比如网络计算、集群、网格技术、云技术、移动计算、P2P网络等，极大地影响了信息技术社会生态甚至是人们的生活方式。区块链也是分布式技术最新的重要发展。

分布式系统特点是没有全局时钟、计算行为并行、可故障容错并满足一定程度透明性地协同合作求解目标，其基本理念是：复杂集体行为可以通过简单个体的自同步来完成。建立互联网思维和分布式思维是理解和研究区块链的基础，凯文·凯利在《失控》一书中提到了很多很好的思维方式。区块链技术也是分布式的一种新的发展，从技术层面看，区块链是一种技术，它融合了很多前沿技术，包括非第三方数据共享，信誉提升，时间轴数据库，价值网络等。但从社会层面看，和以往信息技术不同，区块链又不是一种单纯技术，它涉及和解决了经济，哲学，法律，文化等社会领域问题，成为一种构建社会各种形态和技术的桥梁。

智能合约早在比特币区块链诞生10年之前的1994年，就由密码学家尼克.萨博先生首先提出了，但始终没有推行起来，主要因为它需要一个受信任的计算执行环境，而区块链正好满足了这么一个需要。因此区块链和智能合约的结合成为了第二代区块链的显著标志，并具有划时代的意义。

关于智能合约的目前水平，胡教授认为可以划分为三类：第一类是简单型智能合约：也称链上代码（chaincode）,如以太坊上大多数项目，只是可操作性代码，形式和内容简单，基本没什么智能；第二类是契约性智能合约：是表达契约关系、控制数字资产的代码，如网络购物、租赁、遗产等合约，更为复杂，有一定承诺和约定的智能表达；第三类是代码即法律合约，具有存证和判据，符合法律规制或法律的代码化，是更智能，更高级的合约，将极大影响互联网世界法律秩序的建立和自动判别。应该说，无论是哪一种，智能合约都是代表了区块链上主流的、大规模的应用，智能合约技术是区块链革命中最重要的因素。

现在智能合约还出在早期阶段，有许多问题需要解决，包括最先把智能合约引入到区块链的以太坊，也存在很多问题待解决。经过研究探索，胡教授提出了智能合约工程（SCE）的概念，在形式化验证方面也提出了很多新的理论研究和技术实践。

虽然现在的智能合约还不“智能”，但是这也是正常的，随着越来越多的人关注智能合约，国家层面去考虑设置相关课程甚至专业，对智能合约的发展都有很大推动作用，就比如现在有很多培训机构和区块链学院，也都是一种积极的推动。目前区块链的各种落地项目和应用都离不开智能合约技术了。

未来和人工智能等技术融合，我们可能只需用自然语言表达需求，或利用专业人员提供的契约模板，系统就能自动可信智能合约，届时智能合约将能满足大规模应用的发展。

开场

时艳强：各位布洛克人，大家晚上好！ 欢迎大家来到领先的区块链社群媒体【布洛克科技】，与5000+社群1000000+布洛克人一起参与【时点对话】节目，探讨区块链技术。本期是布洛克科技【时点对话】第153期，主题: 智能合约距离智能还有多远。嘉宾：胡凯。

胡凯，北航计算机学院教授，北航分布式与移动计算实验室负责人，北京市计算机学会理事。曾任新加坡南洋理工大学研究员、法国雷恩一大客座教授和美国亚利桑那州立大学访问学者。主要研究内容包括分布式计算系统、区块链技术和形式化设计与验证方法。

主编了国内分布式计算权威教材《分布式计算系统导论》，是国内区块链和智能合约技术早期研究学者之一；智能合约工程（SCE）和验证即服务（VaaS）等概念和理论方法的提出者，主持完成国内多项重要区块链应用落地项目。

近年来先后主持和参与国家基金、863重大项目、国家核高基及多项大型工程，发表SCI/EI检索论文50余篇，获得国家发明专利和软件著作权30余项。让我们掌声有请今天的角儿：胡凯。

【时点对话·第一问】

“区块链是一个融合的桥梁性技术，构建了社会的各种形态和技术的桥梁”

时艳强： 胡教授，您是北航计算机学院教授，对区块链和智能合约有很深的见解，您是怎么了解到区块链和智能合约的？您认为区块链和智能合约的社会价值是什么？

胡凯：各位【布洛克科技】的朋友，大家好！回答布洛克科技【时点对话】第一问。时总好，各位网友好。我认为信息技术从来没有像现在这样影响人类的生活。我自己长期研究分布式计算，2000年以来分布式计算技术方面有很多进步，有网络计算、集群计算、网格计算、云技术、移动计算、P2P网络等，可以说极大地影响了信息技术的发展、社会生态甚至是人们的生活方式。

应该说，区块链也是分布式计算一个最新的技术发展。关于区块链技术最近有很多说法，比如央视的一个对话节目说它是互联网价值的十倍。我在这里可以概括为两句话：区块链是一个技术，因为它有非第三方数据共享信誉、提升时间轴、数据库、价值网络等许多革命性的应用进步，非常多的应用场景。

但是区块链技术又不是一个简单技术，因为它涉及到了许多社会的领域，比如说早期的一个区块链项目做结婚登记，以后大家也许不用到民政局，而是在结婚登记链上足不出户就能进行登记，类似的场景其实有很多，有可能极大地改进了社会的形态和人民生活的方式，这就涉及到经济、金融、文化、法律等社会学领域。因此区块链是一个融合的桥梁性技术，不仅融合了众多的技术，也构建了社会各种形态和技术的桥梁。

区块链技术为什么如此热，如此受到各阶层、各领域、甚至是非技术人士的重视和热捧，我想是这是值得深思的问题，正如Gartner报告所预言的，数字社会是人类发展的愿景, 智能合约作为新经济范式的基础, 算法会以透明和开源代码的方式，在区块链（BlockChain）中自由设定。这也许是区块链热深层次的原因和推力。

【时点对话·第二问】

 “凯文凯利在《失控》中说分布式给我们带来了一个新的思维模式：复杂的行为可以通过简单个体的自同步来完成”

时艳强： 胡教授早在2014年的时候就写过一本国内分布式计算权威教材《分布式计算系统导论》，那么分布式计算最大的意义什么？有哪些应用场景？目前面临有哪些挑战？

胡凯：回答布洛克科技【时点对话】第二问。这本书是我和我的导师胡建平先生历时五年编著的国家级教材，是国内目前最权威的国家级教材，包括了分布式计算的所有基础理论，包括分布式进程、分布式协议、分布式命名同步、逻辑时钟、一致性、安全等。

其实分布式技术早在上世纪70年代就是大家热门研究的领域，它有几个基本问题：第一，分布式系统没有全局时钟的；第二，由于通信延迟和并发带来了执行的不确定性；第三，它要求具有节点容错能力，并整体上具有某种透明性的。

有一个著名的分布式的基本理论，CAP理论，其中讲到一致性、可用性和分区的容错三者是不可兼得的。区块链目前也有人提出和研究类似的理论来解释区块链遇到的性能等问题。我认为分布式我们带来了一个基本的思维模式：即复杂的行为可以通过简单的个体的自同步来完成。比如比特币系统就是这样的一种模式，其自组织形成了一个历史上最大计算能力、最稳定的一个分布式系统。凯文·凯利在《失控》这本书里面给了很多的分布式思想的解释,

【时点对话·第三问】

“我们认为智能合约是一个软件，但是智能合约又是一个特殊的软件”

时艳强：胡教授您很早就提出了智能合约工程（SCE），您可以给大家分享一下什么是智能合约工程？目前有哪些研究方向？取得了什么成果或者有何进展？

胡凯：回答布洛克科技【时点对话】第三问。这个要从软件工程开始说起，为什么会诞生软件工程呢？在60年代中期，爆发了软件危机，也就是软件的规模化生产以及软件的可靠性成为软件发展的制约性因素。在1983年，软件工程就提出了七条基本原理，包括从语言、数据库到开发工具、平台等方面的定义，它在给定的成本和进度下要求开发出具有适用性、可修改性、可靠性、可维护性等十余个属性的可靠软件。

目前的智能合约也处在一个初期的过程。首先我们认为智能合约是一个软件，但智能合约又是一个特殊的软件。我们研究智能合约的属性，给它定义了十个有别于其他软件的一些属性，比如说智能合约需要有合法性、证据性、一致性、智能性、可信性、可观察性等智能合约作为一个特殊软件的属性。

自从智能合约诞生以来，就发生了很多不可信事件，包括2016年6月的the DAO事件，2018年4月22日到25日，几个公链发生的重大漏洞事件，给客户带来了巨大的经济损失，这是智能合约作为一个特殊软件的特殊属性。因此我们在2017年初，就提出了一个智能合约工程的概念。智能合约工程是融合软件工程、复合验证方法和计算法律的智能合约系统化、规模化的开发过程就是要解决智能合约可信化、规模化生产问题。

我们目前的工作包括对智能合约的形式化验证、并行模型、一致性测试、基于模板和人工智能的合约生成、自动部署和运行、以及法律代码化等一些方面，力图构建一个完整的智能合约工程体系。

【时点对话·第四问】

“对于区块链，稳定性和性能从来都是矛盾的存在”

时艳强：以太坊被称作区块链2.0的代表，即区块链+智能合约，您如何评价以太坊的这种设计模型？我们知道，以太坊饱受诟病的一点就是性能太低，在当前DApp还不多的情况下依然会产生拥堵问题。您怎么看待这个问题？目前有哪些应对方案？

胡凯：回答布洛克科技【时点对话】第四问。以太坊作为区块链的2.0的代表，确实从2015年以来对这轮区块链的热潮起到了极大的促进作用。早期在我们实验室的研究中间也多次请到了以太坊的创始人Vitalik先生来进行交流，我们认为区块链2.0里引入智能合约是区块链的巨大进步。这源于区块链需要一个上层应用的支持，特别是价值转移的时候需要用契约性的、满足图灵完备性的代码，以太坊智能合约实现了基本的框架，是一种划代性的进步。

我们知道智能合约比区块链早提出了十年时间，其提出者尼克·萨博对智能合约给出了一个很好的定义，即明确提出智能合约就是执行合约条款的可计算交易协议，是一个协议性、契约性的代码化，它有基本的契约性质、代码性质以及可强制性的特点。但智能合约一直没有流行起来，这是因为作为一个不可更改的契约代码，它需要一个受信任的计算执行环境，而区块链正好满足了这么一个环境。因此智能合约作为在区块链上不可更改的执行代码就成了价值转移的契约，就好像我们双方签署了一个纸质合约，合约上需要盖一个红章或者盖一个大印，而区块链正好是给代码合约盖了这样的一个大印。

虽然以太坊现在有一些诟病，比如性能太低，但性能这个东西是非常复杂的问题，本质上看大体上目前的解决方思路有几个，一个是加快做块速度，容易导致废块、分链等；第二个是可以增大块容量，但可能导致数据爆炸等问题；第三个是采用多链分布并行，子母链、链上链下互动等，但复杂性和可信性的原因，实用性还不强；还有就是采取一些软件的优化，比如说并行化、算法优化、甚至一些硬件加速等，但改进效果并不明显，尤其是智能合约执行环境下。

从区块链来讲，稳定性和性能从来就是矛盾的，是分布式里头最基本的问题，这种问题可能需要牺牲某方面的利益来达到另一方面利益，因此区块链的性能问题一段时间仍然是重要瓶颈之一，我想还会有很多的发展技术的产生。

【时点对话·第五问】

“形式化方法是一种更严格于软件测试的验证方法”

时艳强：关于智能合约的形式化设计与验证，您首次提出了验证即服务（VaaS）的概念,并发表过一些相关的论文。为什么需要形式化验证？如何实现验证即服务？您可以举一个应用场景的例子，给大家简单介绍一下。

胡凯：回答布洛克科技【时点对话】第五问。所谓的形式化方法其实是一种验证方法，我们平时接触最多的是软件测试，但实际上它只能证明软件有错，而不能证明软件正确。形式化方法是解决软件危机的另一种途径，是一种更严格于软件测试的方法，它以数学方法描述和推理为基础，采用规范语言加形式推理，通过精确的数学手段和分析工具得到验证。目前形式化方法是国际信息安全领域中最高级别安全软件所强制要求的验证方法，大体上可以分为两类，一类叫演绎验证，另一类叫模型检测。

目前大多是采用模型检测的方法验证系统的可信性，主要过程包括模型的建立、模型的转换、模型的验证进行自动代码生成，这样的过程可以反复进行迭代。我和蔡维德教授在美国合作，在2014年提出VaaS的概念，就是验证即服务。在这之前云服务上有很多新的理论，包括蔡维德教授提出的TaaS测试即服务理论，发表了很多相关的文章。

验证即服务的意思是Verificationas a Service，我们把验证作为一种可以在云上提供的服务，对所有的服务可以进行按需定制、组合和验证，并对组合服务进行验证，这样的验证方式和测试方式结合，未来可以支持一些大规模的服务验证和自动服务软件生成，比如智能合约的微服务化、以及服务定制、组会及其验证。

这对智能合约产生非常重要的推动作用，比如我们目前已经用SDL语言对区块链的协议进行建模，采用SDL的工具对建立的私有链模型进行仿真验证，可以验证死锁、活锁等一系列可信性的性质，包括功能性质和非功能的性质。我们也对智能合约采用SPIN的模型检测工具，对智能合约进行验证，并且实现了一些智能合约验证的辅助工具。

【时点对话·第六问】

“ 区块链和智能合约是一种复合技术，涉及到了经济、法律等多方面的知识，这种大融合可能正好是其未来的发展趋势”

时艳强：我们不得不承认，现在的智能合约（Smart Contract）智能合约还不够Smart，经常会爆出有漏洞或者存在安全隐患。您认为现在的智能合约处在什么水平？距离规模性的商用还有多远？有哪些问题需要攻克？

胡凯：回答布洛克科技【时点对话】第六问。这个问题提得很大，现在智能合约确实还有很多的问题，包括智能合约的不智能。目前智能合约基本上是一个固定的合约模板，将来谁来编写，谁来验证、测试和认证，智能合约如何动态地修改，智能合约的执行机制、触发机制、可靠安全保证，合约的合法性，都是我们要面临的一系列问题。智能合约既然是一种契约性的代码，必然要具有一定的法律效力，并且符合法律规制，这都是难点问题。还有比如外部信息源的问题，并发问题，如果多个合约同时执行会带来复杂的同步和并发的一致性问题，还有刚才讲的合约的验证问题等。

我们可以把智能合约简单的分为三类，一类是目前用的比较多的简单的链上代码（IBM）称为链上代码），大多是目前以太坊上项目中简单的IF-THEN-ELSE语句的合约，只是一些可操作性的代码，没有什么智能形式和内容，都比较简单；还有一类可以称之为契约型的智能合约，表达契约关系的代码。比如说购物的合约，比如出租的合约或者追溯的合约，有一定的承诺和约定的智能表达，这些我们可以通过律师或者现成的契约模板，把这些模板转换为代码形成智能合约。另外还有一类代码即法律合约：具有存证和判据，符合法律规制或法律规则的代码化，是更智能，更高级的合约，我认为也是智能合约的最有前途的发展，我们目前在做一些法律代码化的工作。

有一个误区认为智能合约只是绑定在区块链上一个附属品，其实我们如果从智能合约最本质的定义及智能合约的契约性、法律性的角度来考虑，就知道它其实是一类更复杂的应用。第三类代码合约可能是最高级的所谓的代码即法律，具有判决，符合法律规则和法律制度的代码是更高级更智能的合约，而且必将影响我们生活方式，因为人类社会就是契约性社会基础。

我们想，未来的智能合约在区块链的这个革命大潮中一定占有的非常重要的地位。而且我认为可能会在未来占有主导的地位。这时智能合约就会出现大规模的应用和大规模的产生，这样的话智能合约的生产、验证和公信属性就具有了非常非常重要的作用，可能需要建立未来的一个公信生成机制或者生产流程。

在智能合约本身的生产过程中，由于智能合约本身是一种软件，我们在软件工程前期取得的成果都能用得上，测试也好，审计也好，验证也好，各种软件case工具也好，都可以用。但是由于智能合约又是特殊的一种软件，因此要进行许多特殊性的研究，需要解决的问题如何应用契约化，契约如何模板化，其实我们可以看到很多商业合同具有模板化，我们需要契约的模板化，然后进一步是模板的代码化，代码的智能化、法律的代码化以及代码和文本合同的一致性测试。

在这个过程中间，我们肯定可以用到很多包括人工智能方面的一些成果，比如自然语言识别方面的一些研究成果，可以把文本自动代码化。因此总体上来讲，区块链和智能合约其实是一种复合性技术，涉及到了众多的经济学模型、法律方面的知识，而这些大融合可能正好是未来的发展趋势。

【时点对话·第七问】

“区块链涉及到包括计算机、法律学、金融系、数学、计算群体工程学、密码学等等方面交叉性学科”

时艳强：区块链和智能合约还是比较新的技术，行业相关人才缺口比较大，国外已经有大学开始设置相关的课程甚至专业，那么我们国内高校状况如何呢？胡教授深耕分布式计算系统和智能合约等相关领域，您对未来的课程设置或者专业设置有哪些期许？

胡凯：回答布洛克科技【时点对话】第七问。这个问题也非常复杂，我其实最近也注意到有些高校宣称要设置区块链的专业或者是开设区块链的课程。但实际上从教育来看，设计正规的学科专业并不容易，我们知道最近国家特别批准设立了网络空间安全这个学科专业，也是经过了很多年的实践才得到批准的。

设计一个学科专业，需要学科的基础理论体系，体系化、系统化、基础化等等，而区块链涉及到了很多交叉融合的学科，比如包括法律学、金融系、数学、认知、计算群体工程学、密码学等等，是需要综合进行学科设置的。

很多业余的培训机构或者各种各样的区块链学院都对区块链的发展起到了一定的促进作用。当然我们更期待于各种学校体系和高校体系能够进入到区块链的人才体系来，这样才能根本解决这个区块链的人才结构的体系。我们国家已经是区块链和互联网方面的大国，但是我们在互联网发展和知识产权上吃了很大的亏，和我们互联网大国的地方不相称。区块链属于一种朝阳性、初始性的领域，在这方面，我们完全能够建立我国自主的知识产权和自主的理论知识体系，我想这也是我们要奋斗的目标。

作为国内最早开始区块链研究的高校，北航计算机学院从2014年开始就成立了区块链和数字社会实验室，是当时由蔡维德教授牵头，包括了清华、北大、北科大等首都的一些高校的老师，包括以太坊的创始人V神，还有一些国外的院士都是我们这个开放平台的研究合作者。在此基础上，我们也进行了很多区块链学术方面的早期研究，包括我前面说的智能合约，还有计算法律学方面，还有密码学方面等，在国内也创造了我们自己的北航链，在国内外产生了重要的影响。

【时点对话·传承问】

时艳强：胡教授作为资深的区块链领域研究者，应该接触过很多行业内人士，其中是否有您欣赏和佩服的从业者，为什么？【布洛克科技】目前覆盖15个国家250个城市5000个社群节点用户100万+，希望通过【时点对话】邀请更多的大咖来社群分享区块链，以推动整个行业进一步的发展，如果胡教授引荐两位嘉宾，您会引荐谁来做客【布洛克科技】进行分享？

胡凯：回答布洛克科技【时点对话】传承问。国内方面现在区块链的研究者很多，我看了工信部的白皮书，去年以来就成立了四百多个区块链公司，包括BAT企业也在高调宣称布局区块链，但其实真正的落地应用、特别是一些大型的应用目前还比较少。我们看到了区块链技术的一些被看好的前景，包括马云先生在前不久的一个主题报告上特别提到了三个未来的技术，就是人工智能、物联网和区块链，而这三者其实是可以互相融通的技术。

国内高校的区块链技术团队有很多了，我了解的比如说清华大学邢春晓教授、北京科大的朱岩教授、同济大学马小峰教授的团队，还有一些做形式化方法的国外的合作者，比如法国Jean Pierre教授及其同事们，他们用F*语言做智能合约的验证，还有我北航同事蔡维德、伍前红教授等，此外、浙江大学、同济大学，北邮、中财等都有很多杰出的区块链技术的推动者和研究者，区块链技术在国内应该说具有了越来越广泛的研究和从事技术开发的人群，这也是我们国家应该能站到区块链的高端和引领地位的一个基础保证。

【时点对话·提问一】

问题一：胡教授，请问一下，智能合约的编程语言与传统编程语言有哪些差异？学习智能合约的编程可以从哪里入手？——来自【布洛克--西安交通大学--001】

胡凯：回答布洛克科技【时点对话】提问一。目前智能合约有一些编程语言，大家用的比较多的应该是以太坊的Solidity，其实我们自己设计的智能合约就是采用了Java，用Java的反射机制设计了智能合约执行，我觉得各种语言应该是都可以的，跟着主流的语言学，一个好处可能就是也许将来他会成为一个标准，但正如我们可以用各种语言编程同一个应用一样，并没有什么太大的差别。

如果大家习惯用Java也可以用Java。我了解到现在有些人还在做统一的平台或者未来的智能合约语言的一些内容，一些更高层的语言。例如我刚才讲的形式化方法的描述语言可以转换成底层的语言，比如说Java语言或者C语言，这样可更方便支持非专业用户的编程。

将来最方便的是我们给大家一些编程的接口，或者说一些智能化的一些工具，比如只需要用户来写一些模板，甚至用自然语言来输入你的诉求，就像你写一个纸质合同的模板一样，然后软件工具可以自动把他们变成任何一种系统都能接收的智能合约语言。如果大家来学习一些智能合约的编程语言的话，我想一些常用的方法和语言都可以，现在都有很多相关的介绍和介绍书。

【时点对话·提问二】

问题二：胡教授，在开放的区块链上，任何人都可以参与并上传编写智能合约，比如以太坊，那么如果有人编写了病毒式的智能合约，这对区块链的安全显然是不利的，如何防止这种情况出现呢？——来自【布洛克--中国科技大学--003】

胡凯：回答布洛克科技【时点对话】提问二。这是一个很有趣的问题，因为分布式系统一个重要的特点就是要开放参与，开放参与里头也难免有一些要捣蛋的人，我其实还没有碰到过这种事情，不知道有人碰到过没有，比如说有人编写了一个病毒智能合约，在以太网上能起到一个什么破坏作用。我想现在编智能合约，上一些系统的时候，首先是需要审计的，需要测试一些功能，但矛和盾永远都是在一个双向互相攻击的过程中得到技术发展的，这种事情肯定会有，但这不是、也不应该是我们发展的主流，就像我前面讲的智能合约工程产生的一个重要的原因就是智能合约必须是具有法律规制的。

如果说未来智能合约出现这种情况，首先保证它的还是法律因素，我们说要从法律上来解决智能合约的安全性问题和技术方面来解决智能合约的可信性问题。因此现在区块链技术，包括区块链的监管、智能合约策略的可变性机制研究，也是可能的研究热点。

 （感谢胡凯的分享，也感谢每一位布洛克人支持）

——布洛克科技·简介——

【布洛克科技】是领先的区块链社群媒体，集新闻、快讯、行情、社群、项目为一体综合性服务平台。全球首创“社群媒体”概念，7*24小时项目追踪报道，秉持“客观、真实、深度”的理念，服务全球区块链领域创业者与投资人。