DEVCON2: 基于规范程式逻辑L4合约编程语言的设计

记者：Lydia

来自一家新创公司名为Legalese的技术专家Dr.Virgil Griffith， Vikram Verma演讲主题是基于规范程式逻辑L4合约编程语言的设计。

L4背景介绍

Dr.Virgil Griffith：L4是可以让律师使用的特定语言。Vitalik会对这个语言进行形式化验证，当然这是玩笑。

如果合约出现bug，有些人说可以直接起诉，但是这个成本是十分高昂的，损失会非常大。我们希望我们的用户更加了解我们的语言，比律师更加了解。因此我们要讲的是为什么开发L4语言，一些律师也开始拥抱这个语言。

我们在实际的以太坊程序中使用的以太坊合约和L4模态，大家可能会问，我们已经有了Solidy语言，为什么还用其它的？对于有创意的应用可以用Solidity，对于更加高级的应用我们要考虑一些实施细节。L4可以映射到法律体系中，通过这样的语言，可以编译成法律所使用的语言，可能很多律师会转行到以太坊，因为他们觉得以太坊更加可靠。

我们已经和以太坊签署了一份价值9000万美元的合约。

同时已经达成共识，接下来要做的就是对文献的回顾、如何推理这样的语言以及通过什么方式将语言编成代码。

Vikram Verma对此进行了编程上的详细解释

如果你做了a就必须执行b，如何你做了a没有执行b，你就违反了合约的规则。

有一些语义学已经界定到其中，有些可以被其它表达所替代，这里是合约运行合约的监测。有一些恶后果是由于一些合约造成的，执行a的结果是完成之前合约里的事件，你想完成一些界定的关系，。如果想在同一时间执行很多关系，就要遵循相关规定。所以我们看到如果你违反的结果就是失败。

我们可以把这些事情转移到机器上，机器会告诉你的这些抱怨是否是合理的。这里图表最酷的部分就是在于可以对一系列事情进行分析，可以进一步查看是否能够满足。

另外一个有趣的一点是如果你考虑了做了A和b同时的结果，进行同时验证，我们也可以选择是否执行b，有时候会出现一些争议。

Dr.Virgil Griffith补充到，

你们之前看到的是一个非常好的编译合同的方法，但是问题出现时责任该归谁。当一个人没有完成职责的话，并说出来了我们就可以对此进行处理。我们可以假扮法官进行判断：当前合约出现的问题，有了这个合约我们就知道责任归谁。

这里也有一个时间戳，每个合同都被定义为一个函数，每个函数都有自己的组成部分∑。所以我们可以通过不同合约的展示看出语言的魅力，比如说R是一个义务条约，K表示的是行动，如果满足的话就可以执行这样的合约，所以通过这样的方法就可以把合约连接到一起。我们首先要找出合约不同的结构，最终决定谁应该负责。

另一个合约例子，如果你进行调用，他的参数是雇主，你就可以设定一个时间戳，最终可以裁定员工是否违反合同规定，这些员工规定可以编译为合同语言。

这里是其它的语言应用，我们还有另外的限制和复杂的情况，因此可以按照我们想要的方式进行编制。

Vikram Verma阐述道关于合约的变化以及升级我们有非常好的想法，通过合约可以更好的界定合约和义务，可以让合约正常化。

作者：Lydia | 来源：Chainb