历史匿名回执 ·
课程内容： 前半程简直是coq新手村的阳光大道，基本语法配trivial式证明，一路平推到用coq证程序性质，用coq写Hoare Logic和Monad的证明。此处体验丝滑得像热刀切黄油，课上干货密度堪比压缩饼干，（个人觉得）内容挺有趣，作业量还不大，属于是天堂难度。 但后半程直接一脚油门开进**劝退峡谷**，想选课的务必系好安全带慎重选择。后面的大块内容全是拿coq写Separation Logic相关证明、搞c程序符号执行。核心雷点：coq原生不支持分离逻辑内存相关的谓词，这块只能用老师自己开发的一个工具来写证明。缺点清单如下： - **做作业没法从网络或者gpt那里获得帮助**，要么自己原地悟道，要么高强度骚扰助教（在此对被我反复轰炸却依旧耐心解答的助教献上膝盖）。 - **配环境十分甚至九分的折磨**。上课的几个人整整花了一个星期才把环境整明白，教室的机器一开始也没装好，后来助教又燃了半个小时才弄好。本来_CoqProject里面各种逻辑路径已经让人脑瓜子嗡嗡的，还得手动写Makefile、调vscode插件参数、设docker映射路径，这一套下来感觉自己不是来学验证的，是来当运维的。 - **工具存在各种各样的bug**。问学长，似乎去年他们也用这个工具写大小作业，所以我们摸到的已经是debug过的版本了。然而该抽风还是抽风，比如符号执行工具一遇到c语言的enum type就直接躺平（fixed）。助教那边修bug的latency比较高，有可能一个trivial的bug就把大作业进程堵死半个星期（我对此表示理解，但身体的难受是真实的）。 - **作业workload高**。这和进入Separation Logic之前形成鲜明反差，在那之前基本每周作业不超过一个小时就收工。踏入分离逻辑阶段后，不光要写coq证明，还要写c符号执行的前后条件，一旦发现自己某个证明的前/后条件写得太强/太弱，恭喜，c符号执行重写、coq证明再调，循环养猪。分离逻辑有一个小作业一个大作业。小作业是证明c里面一个双链表FIFO队列的性质（入队出队函数的前后条件）。大作业从几个选题里选一个，疑似每一届的选题都不一样。据不完全统计我整个大作业至少写了**4000**行代码，其中某些证明公式化copy paste稍微改一点就Qed，就算把这些灌水部分刨掉也至少有**2500**行不重复的代码。选前问学长，得到的回复是他们的大作业大概1000行代码左右，尚且不知是不是个例。 上课自由度： 点名？不存在的。这门课今年选的人只有个位数，谁没来那叫一个鹤立鸡群，即便这样也没扣分。来了线下会提醒你注意听讲不要玩手机。 考核标准： 大小作业，无考试。 授课质量： 上面那堆牢骚全冲着qcp工具和作业不合理的地方去，单纯聊授课质量那真是无可争议。老师的水平毋庸置疑（无论理论还是coq各种证明技巧），卡壳的地方找老师，三两下就能给你点通。上完这门课也确实感觉自己肚子里多了不少货，~~只可惜和本人方向不太match~~。权当给自己的技术栈又砌了一块砖吧。