Hi Tunars,
众所周知，写出正确的代码从来都不是一件容易的事。虽然不写代码就不会有bug，但是不写代码是不可能的。为了从逻辑上证明某个程序满足某些想要的属性，我们必须采用比测试更加重量级的形式化验证手段。定理证明是一种能验证几乎任何（使用高阶逻辑）属性的证明方法——只要你知道这个定理该怎么证明。这次讲座以知名的证明助理
Coq 为例，从初学者的角度介绍其基本使用。
活动信息：
* 主讲人：朱俸民
* 时间：2020/07/04 19:00 UTC +08:00
* 活动形式：线上会议 + 直播
* Zoom：685 7505 8025
* Zoom 直播：https://live.bilibili.com/699121
欢迎一起来玩！
--
Shengqi Chen
--
您收到此邮件是因为您订阅了 Google 网上论坛的“TUNA 主邮件列表”群组。
要退订此群组并停止接收此群组的电子邮件，请发送电子邮件到tuna-general+unsubscr...@googlegroups.com。
要在网络上查看此讨论，请访问
https://groups.google.com/d/msgid/tuna-general/553a04a8-4cc2-44b0-a3f7-acc0baea5b36n%40googlegroups.com。
