Leslie Lamport-分布式系统的祖师爷

中本财经TACHION专栏

作者 ： TACHION天念

在区块链的设计中，保证所有参与者能够正常的在网络上通讯，并且能够使各个节点正确的达成共识，区块链需要面对系统中节点作恶的情况。因此在设计区块链时，我们需要有能够正确指导区块链共识设计的理论。

智能合约的火爆带来的DAPP的安全性问题屡见不鲜，因此有人提出对智能合约形式化验证的方式保证合约的正确性，然而有能力完成这样工作的人寥寥无几，学习难度也极高。我们需要一个适当的工具来辅助我们对只能合约进行验证。

幸运的是，这些问题在80年代就被人提出发现并提出了解决的方案，当时并没有区块链的概念产生。解决这些问题的人叫做Leslie Lamport。

Leslie Lamport是分布式领域的重要奠基人，现在微软研究院工作。他为分布式系统基础编写的论文成为了计算机科学史中被引用数目最多的论文。在2013年获得图灵奖，在2000年，2005年，2014年获得Dijkstra奖。

他提出的拜占庭将军问题为现代区块链共识算法的设计提供了理论支持，而他提出的Lamport时钟也成为了现代区块链共识算法与传统共识算法结合研究的重要桥梁。这些论文都是Lamport教授于80年代完成的论文，却成为了现在区块链设计中重要支柱。

另外一个重要的影响是他提出了一种对代码进行形式化验证的逻辑预言TLA+。在这门语言的基础下，我们才能够对现在区块链上执行的智能合约进行形式化验证，确保其执行的正确性。

Lamport教授的贡献不仅仅局限于分布式系统领域，现代常用的排版系统LaTeX就是他所编写与实现的，使得原本难以使用的排版工具TeX能够方便快速的使用。因此LaTeX已经成为各大高校，期刊的论文标准文档格式之一。

严格来说，区块链的基础理论体系“古已有之”，而在这么多年对分布式系统的理论研究也变相的促使了区块链的出现于产生，未来相信在更多计算机学界，工程界的努力下，区块链的会发展的更棒。