2013年图灵奖得主 Leslie Lamport 专访：程序员需要更多的数学知识( 三 ) 作者｜李梅编辑

Lamport：Coq的目的是解决真正的数学问题，它能够捕捉数学家所做的推理。例如， GeorgesGonthier用它来证明了四色定理（four-colortheorem）。一个数学命题的证明经过机器验证后，几乎可以肯定该命题为真。
TLA+不是为数学家设计的，而是为希望证明其系统特性的工程师设计的。 20世纪90年代，在花了大约15年的时间编写并发算法的证明之后，我了解到为了证明并发算法的正确性需要做什么。 TLA是能够一种让证明过程具有完全的形式化的逻辑，而且TLA+也是基于TL逻辑的一套完整语言。
Quanta：像TLA+这样的规范语言在工业中使用得不是很广泛，是吗？您认为这是为什么？
Lamport：我正在尽我所能。但基本上，程序员和许多（如果不是大多数的话）计算机科学家都被数学给吓坏了。所以它的「销路」很困难。
另外，每个项目都必须急匆匆地赶完。有句老话，「永远没有足够的时间把一件事做到完美，但总是有时间去重新来过。」因为TLA+涉及到前期工作，在开发过程中又会添加新步骤，所以这也导致了它没有被广泛使用。
Quanta：前期的工作是否总是值得的？
Lamport：的确，世界各地的程序员编写的大多数代码都不需要非常精确的语句来说明它应该做什么。但有些事情很重要，需要保证正确。
例如，当人们制造芯片时，他们希望芯片能正常工作。当人们构建云基础设施时，他们不希望出现会丢失人们数据的bug 。对于那些要求精度的应用程序，你需要非常严格。而且你需要类似于TLA+的东西，尤其是当涉及到通常存在于这些系统中的并发时。
Quanta：程序员是否倾向于花更多的时间去写代码而非思考代码？
Lamport：是的，在编写代码之前进行思考和写作的重要性，需要在本科的计算机科学课程中教授，但事实并非如此。原因是教编程的人和教程序验证的人之间没有交流。
就我所见，这一分歧的两边都存在问题。教编程的人不了解他们需要知道的验证，而教授验证的人不理解它应该如何应用和在实践中使用。
在弥合这一鸿沟之前， TLA+是不会收获大量用户的。我希望我至少能让教授并发编程的人明白他们需要TLA+ 。那样的话， TLA+也许还有希望被更多人使用。
Quanta：我感觉到，您对近年来的计算机科学教育不太满意。是不是因为对数学重视不够？
Lamport：是的，在数学思维方面。
Quanta：那么，您会如何构建本科课程？
【2013年图灵奖得主 Leslie Lamport 专访：程序员需要更多的数学知识】Lamport：我不是一个教育家，所以我不知道如何教他们。但我知道人们应该学到什么。他们不应该害怕数学。他们可能学过一门简单的数学，但不知道如何使用它。他们不知道这有什么好处。他们学了足够多的知识，通过了考试，然后就抛之脑后。
Quanta：数学家常说他们在数学中看到了美。你是从算法领域起步的，那么您看到算法之美了吗？
Lamport：我并不从美学的角度来考虑。我可能和其他人有同样的感觉，但我只是用不同的语言来表达。关于算法，我考虑的不是美，简单是我非常看重的东西。
参考链接：
https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/

文章图片
雷峰网