曹钦翔 · 程序语言设计与实现修读档案

曹老师那是真强，我只能说这门课coq含量过高，是它最离谱的缺点，虽然我自己这门课没到80）））

和楼上属于是赛博击掌了，楼上那份课程测评写得比我体测成绩还客观。说实话我也想多啃点编译原理的硬菜，而不是被coq证明按在地上反复摩擦，最后几周的课coq浓度高得像直接往血管里灌，感觉对以后不搞形式化方法的兄弟姐妹来说，编译器前端加解释器那部分知识才是真能揣兜里带走的干粮。（当然，也可能学coq顺手把大家的逻辑推理能力给升级了一下） 抛开课程内容这套配置不谈，曹老师的授课质量是真的顶，老师那思维水平感觉自带降维打击buff，经常让我产生一种凡人在仰望神仙的错觉，只能膜拜。

### 课程内容 （据说和去年的不太一样，嗯，据说） 词法分析、语法分析、程序语法树、指称语义、小步语义外加它们互相转化、简单解释器，一整套流水线给你端上来。全程Coq当电子榨菜陪着，干嘛用的呢——证明语句的正确性（e.g. 这么定义的while循环，它真的是一个符合直观表述的while循环，不是披着while皮的if）、证明转化的等价性，诸如此类，主打一个"我说的对，机器也点头"。 ### 评分构成 - 课堂参与10%（每次发言+1，点名缺勤-1，最多容错两次）——发言是存款，缺勤是扣款，账户只准爆两次 - 小作业40% - 大作业25% - 期末25% 其中，小作业的给分是3分制，向下取整。有时候会很亏，比如7/11就只有1分了，数学在这里展现出了它最冷酷的一面。听说最后有调分。 大作业有前端实现、解释器、Coq证明等选题。**题目难度的标准差很大，** 且不同组不能选一个题目，等于开局就是一场抢题生存战。好题目可能一两周就搞定了，但需要抢，手慢无。其余题目也不是不能做，就是工作量略高——高到你会开始思考人生的意义。 大作业分数构成为： - 完成分（满分 15 分） - 难度分（满分 6 分。每个题目会有三档要求） - 第一档难度，得 6 分 - 第二档难度，得 3 分 - 第三档难度，得 0 分 - 组队分（满分 4 分） - 选择有额外难度的题目（需与老师提前沟通）、独立完成或 2 人组队完成，得 4 分 - 3 人组队，得 3 分 - 4 人组队，得 1 分 作业布置的频率略为抽象，抽象到什么程度呢——比如第一个月有10次小作业，有可能一节课下来布置三个小作业，分别为理论题/代码题/Coq证明题，一节课三连击，人还没下课魂已经交了三次。但自从布置了大作业之后就几乎没有小作业了，少到我为期末考试感到没底，从"作业轰炸"直接切换到"作业真空"，中间没有过渡动画。 ### 授课质量 **极高！** 老师课程的信息熵适中，如果认真出勤真的能学到很多知识——注意关键词"认真出勤"，翘课的话信息熵是多少就不好说了。有问题可以随时打断老师，老师在比较难的部分也会抽同学回答问题以把你从走神状态拉回来（不计分），属于免费的灵魂召回服务，不计分。感觉课上的真的是有用的，且课下也不用额外花太多时间。 ### 美中不足 Coq证明略多，这部分听起来还是非常枯燥的，感觉未来不想做形式化验证的同学可以略过——翻译一下：除非你打算一辈子跟证明器过日子，否则这部分就是大型催眠现场。 ### Update **Coq证明实在是太多了...感觉后半学期啥都没讲** 降一分，一分，全部身家降一分。 总评给分未知，考后更新。

课程内容：整体讲的很杂，从语法分析，词法分析到寄存器分配，其中还会讲一些数学相关知识，知识的摊位摆得比庙会还热闹。没有固定参考书，那就默认大家都是野路子出道。 上课自由度：低 助教会查签到，不到会扣分，自由不过两秒钟。 考核标准：10%课程回答分（最高可到12抵消缺勤），40%编程分，25%paperwork 25%期末，期末考前会发样卷，很有参考意义，考前发粮，颇有正道之光。 授课质量：高，老师很愿意回答问题，但给人以一定压迫感（可能和老师本人过于出众的经历有关）作业是3分制，给分向下取整，非常折磨，每次交作业前都心惊胆战，宛如赌场里按刷卡键。但最后给分似乎不是直接按百分比给，而是分段给分，属于有惊无险的最后关爱。