众所周知，写出正确的代码从来都不是一件容易的事。虽然不写代码就不会有bug，但是不写代码是不可能的。为了从逻辑上证明某个程序满足某些想要的属性，我们必须采用比测试更加重量级的形式化验证手段。定理证明是一种能验证几乎任何（使用高阶逻辑）属性的证明方法——只要你知道这个定理该怎么证明。这次讲座以知名的证明助理 Coq 为例，从初学者的角度介绍其基本使用。
活动信息：
欢迎一起来玩！
清华大学 TUNA 协会原名清华大学学生网管会，注册名清华大学学生网络与开源软件协会，是由清华大学网络技术和开源软件爱好者、技术宅组成的团体。现阶段向校内外提供开源软件镜像等服务。
The best team on the planet.
