在这段视频里，Clarkson介绍了形式化方法的应用范围，两种古老的形式化方法（的名字[二哈]），三个让形式化方法感觉很无力但又无法逾越的数学定理；以及两个形式化方法的成功故事。

++++

逻辑学的数学定理没法在这么段的片幅里阐述。

Syntax和Semantics，如果你不熟悉这一对术语的话，Syntax是语法，Logic语言和编程语言使用几乎一样的方式构建语法，就是如何inductively的组出字符串（逻辑表达式和编程语言写的程序都是字符串）；Semantics是语义，是一段字符串的『意思』。

经典逻辑的语义是true/false，直觉逻辑的语义是proof（BHK interpretation），直觉逻辑的语义其实不直觉，反而是经典逻辑的语义很直觉，true/false，无懈可击；但直觉逻辑在Coq里的重要性极高，在程序语言里的重要性极高，后面会学到。

程序语言的语义，你会用的语言你当然知道自己写下的代码是什么意思，这是直觉的理解。严格的定义程序语言的语义有很多种方式，operational semantics是最常见的，它是compositional的，即一段合法代码可以拆成更小的代码碎片的组合，而它的语义也是这些碎片的语义，根据语言的操作语义组合出来的。

想更多的了解编程语言的语义可以找本书看看，很多书都可以的；但是语义和这门课的关系不大，因为。。。你看完视频就明白了。 http://t.cn/A6oNNX54