DEVCON2: Lucius Greg Meredith论智能合约的行为类型

记者：Lydia

来自以太坊的LuciusGreg Meredith演讲的主题是：智能合约的行为类型

Greg Meredith自己的蜂巢，事实上，分布式科学是真实的事情，它存在于周边野生的环境。

不同领域的出现可以让形式化验证成本降低。

现在新型的现象正在兴起，我们认为这样的领域在不断成熟，我们有许多例子，除了JAVE和C++以外的领域，可以发现有泄露的软件。当然我们有一系列的应用和安全保障相关的应用，通过这个我们可以降低形式化验证成本，因为我们知道许多程序都需要形式化验证，因此不同领域的出现可以让形式化成本降低。

DAO的缺陷，可以被称为是重要使命系统的缺陷，基于区块链技术架构之上的全球智能合约是这个系统的关键。

我们要解决这样的问题，解决方式如下几点：

可以想象信息流动管理的一些方式，所以这是比较陈旧的观点，关于信息获取。

另一个方法就是在新的执行的背景下插入一个程序，我们之前讲的旧观点可以在另外一段获得输出，我们的程序就像完整的CPU，什么时候可以插入整个模块，让系统运作更加高效，在互联网规模下，我们已经实现了这样的想法，这些实际上都参考了刚刚想到的想法，如果客户想获得来中国的签证，一切准备就绪，但是Visa的漏洞。在区块链的世界中，我们有基于区块链的服务就可以填补这样的漏洞，这是我们讲的行为方式，智能合约有许多不同的行为方式，也有许多错误。

DAO重放攻击变成races的条件，在分布式系统中，谁获得了没法复制的资源是非常重要的，也就是说谁是第一个获得是关键。Rholang是基于区块链的情境，每个合约会出现一些危险的情况，我们希望给予更多的交易量，来保证功能。所以表现的类型不仅会发现races，而且会发现许多其它事情，当合约变成共同合约或其它合约。

第二部分，所有的集合比如list 都是来自monads，左边有一些小例子，就是monads的一些程序，在编译器上首先会发到第二通道，所以我们可以做些非常不可思议的事情。首先我们可以获得的一个程序，就像刚刚讲的程序语境，可以称为鸟妈妈，用programmar填补这个洞，我们主要是定义不同的表现行为，这已经被形式化。C和T组成了一些程序，这些程序和集合进行转换。最上面的是不同类型的语义学的内容，左边C 、T都是使用编程语言的指令，以及不同的编程类型，我们可以用不同的编程规则来组合C和T，提取一些字符串，这是非常简单的。通过这些算法已经中Rolands里面做过，可以用来生成一些类型的系统，可以生成Solidity行为系统。

作者：Lydia | 来源：Chainb