这本书再推荐一下。作者之一是德国国家科学院院士，Isabelle/HOL的主力开发者，并且因此成就获得2021年的Herbrand大奖；Nipkow还有一本很有名的书是Term Rewriting and All That，合作者是Baader，Baader是2020年的Herbrand大奖获得者，主要贡献在自动定理证明的理论领域。

Concrete Semantics前面极速70页介绍Isabelle/HOL的使用，然后讲解了一个简单的类C语言的语义证明，所谓语义证明就是证明程序正确。

用20万行证明代码证明了大约9000行生产代码的seL4操作系统微内核是目前计算机语言和定理证明交叉领域的重要成就之一。是使用Isabelle/HOL完成的。另一伙儿法国人搞的大项目是C语言编译器Compcert，是用Coq的。

++++

不要以为AI时代形式化方法就过时了，相反，恰恰是那个20万行惊悚的proofscript和9000行生产代码都可以用AI完成，人只要看懂证明的结构和命题是自己想要的就行了。

这是AI自己就可以判定代码正确与否，不再输出屎山让人来维护的最重要的手段。