程序语言与编译原理 · 修读回执档案

上课自由度：本来还能喘口气的课后作业现在原地转生成了小测，自由度为0，自由度直接躺平交白卷 考核标准：这每节课小测是要顶替作业的生态位了吗，因为ai起飞所以不布置作业改埋伏小测吗，本来是保平时分的东西现在毕业变身成催命符了，小测还挺正式，电脑手机一律收走，然而我亲眼看见前排有人拿手机偷偷搜，考的东西给的做题时间短到你怀疑人生基本做不完，所以是不是要偷摸举着手机凹搜索才保得住平时分啊，我不想平时分当场核爆，或许这锅得算我头上吧......

课程内容： 上课自由度： 考核标准： 授课质量： 求求了教务，把这门课改成选修课吧，真的听不懂曹大师讲的coq，我感觉自己是在用肉体接航天发射密码。

2026年1月23日：出成绩更新 曹大师发功了，期末成绩直接开根乘10，一通操作猛如虎，最后总成绩居然还过得去。 所以加一颗星，嘿嘿。 不过我那coq小测实在拉得离谱（35/100），平时分照样被扣了5分，薅我一撮羊毛。 --- 2026年1月7日：考试结束更新 这卷子和往年卷子简直不是一个物种啊？总共七道题，就两道题会做，剩下好几道看都看不懂……尤其是不动点定理居然能和活性分析叠一起出一道证明题？？？这是碳基生物能想出来的题目吗。还有这个assume是啥？复习的时候压根没翻到过。第一题NFA一脸人畜无害，真下手了根本写不出来，啊啊啊。 上考场半小时，一道题都没做出来，然后曹大师一直在我旁边晃来晃去，还盯着我解答看，我当时真的当场心态爆炸。 我嘞个豆。 我来逐题点评一下： - 第一题：写出 NFA 对应的正则表达式。 - 点评：看着像只乖猫，结果这 NFA 和上课举例的那些简单结构完全不是一个路子，它有两条互相交叉、纠缠的路线，构造直接卡死当场。 - 第二题：写一个上下文无关语法，来规定 `&&` 和 `||` 以及 `!` 的先后顺序，并且这里的 `&&` 和 `||` 之间是同一优先级的。然后做一个移入规约分析。 - 点评：这道题还是能做的。 - 第三题：在 SimpleWhile 中引入 break，然后试着定义这一情况下程序的指称语义。 - 点评：看不懂，不知道怎么入手。 - 第四题：结合活性分析与不动点定理的知识，构造一个函数，说明活性分析的结果是这个函数的最小不动点。 - 点评：最难读懂题目意思的一题，题干看着就很复杂。证明“不动点”是容易的，但证明“最小”这一步，我不太会。 - 第五题：在 SimpleWhile 中引入非确定性赋值，判定此时的 while 语句的指称语义的 inf 集合是否是某个函数的不动点。 - 点评：还是不知道要干嘛，感觉上是伪命题，但不知道怎么说。 - 第六题：写出集合单子中 assume 和 bind 的定义，并证明 assume-bind 推理的正确性。 - 点评：啥是 assume？复习时根本没看…… - 第七题：定义一个 swap 函数（交换两个内存中数据的位置），写出符号执行过程以说明其正确性。 - 点评：最像人类的一题，非常简单。 --- 2025年11月26日 19点40分： 我觉得这 coq 语言太傻逼了，又要求每一步都必须完全正确，不能出错，结果自己又搞一堆省略写法，或者搞一些另外的符号，美其名曰语法糖，其实这糖是鹤顶红味儿的，要把我毒死了。 无语了…… --- 课有点难，而且老师讲得有点抽象，不太好学，尤其是coq出现之后，真是一头雾水。 等我后面继续更新。 --- coq小测，180分的题目，我拿了35分，哈哈哈🤡🤡🤡🤡 我还准备了一晚上+一上午…… 带着你的coq一边去吧。 小测占总成绩10分，哈哈哈，牛逼了哥们😭😭😭 --- 这coq是人学的？我感觉自己也不算笨，但上到后面根本听不懂，看代码都费劲，还搞coq证明，合适吗？我提议这门课改成选修…… ---- 12-31更新： 复习时才感觉到，曹大师的讲义真是言简意赅，现在整理笔记，有种为《春秋》作传的感觉。哎哎，曹大师什么时候能照顾一下我们这些笨蛋，把讲义写得详细一点啊。

课程内容：coq 上课自由度：低 授课质量：还行，但是coq这玩意儿以后基本查无此人啊。我绞尽脑汁也想不到这辈子什么时候还得跟coq再续前缘。 课程workload大到离谱，我就纳了闷了，大三花大量时间跟coq死磕到底图个啥，是图它证明不了我的人生吗。

课程内容：编译原理含量少得像方便面里的牛肉粒，coq证明含量多得像不要钱的白开水。 上课自由度：还行，人少到一定地步就挨个点名，中途来也行。课上会提问，但你爱干啥干啥——反正也听不懂。 考核标准：平时作业35+出勤5+期末30+编程作业10+理论作业20。 授课质量：没上过的尽管来一起喷，不必划走。 1. 授课内容，大伙都以为是来学编译原理的，结果拐进了程序语言，满屏coq证明。请问c老师，学程序正确性证明对我未来有一丁点帮助吗？为啥把你的科研直接扣学生头上？这是纯纯浪费我们时间，对您又有什么好处？？ 2. 考核标准，上一届学长的大作业是编程作业理论作业二选一，但据说难度差得肉眼可见（这谁看不出来啊）。于是天才的c老师本学期抛出天才构想：**大家都要做理论作业和编程作业**，这不就公平了吗？*nmlgb*一个学期两个大作业加期末考试，大作业里还塞着超绝coq证明，这是碳基生物想出来的？？ 3. 大作业选题，文档写的是先来后到分配，但c老师给隔壁组分编程作业时开始随机乱发。**理论作业选题时一点任务详情都不给**，你只拿到一个题目，难度全靠自己猜，分配好像也不是先来后到，还有一个组邮件直接石沉大海。 4. 大作业难度，隔壁组据我所知好像1800行证完level3，而我们组几个level难度毫无区分，难度曲线是高原，**光算法定义就甩了400+行代码让我们自己啃，里面甚至还有bug**。**小组最终证明代码近10000行，换来理论作业50%左右的分数**。请问c老师出题时到底有没有考虑题目难度不一样？还是您压根不知道这题什么难度？选题的时候都不知道要证啥，难度全看抽盲盒。跟c老师交流下来的观感就是：他随手编了几道题，写个算法一丢，具体怎么证我怀疑他自己都不知道。 + 顺嘴提一句，最后好像是4/6个组做完了证明，但我不觉得是我们组能力有问题，我自己确实没怎么搞明白，但我的义父们绝对不比别的组笨或懒，我觉得我们组的任务就是比别的组难。我也不认为cqx本人能在短时间内证完这个命题。另外，我们**大作业里用到的某处定义十五周才开始讲，十六周周五才讲完**，诗人我吃。 5. 答疑，包括但不限于：，"老师请问我们这个方向能证通吗""你们自己证试试，能通就能通，不能通就不能通"；"我们没证过题目，给出的定义可能有问题，是因为你们开始证明太晚，没及时发现"；"请问老师定义是不是错了""自己判断是不是错了，你们觉得错了自己改过来就行"。 6. 期末，最后两题单子和分离逻辑，单子感觉跟上课讲的形式完全不沾边，分离逻辑丢你一段单链表c代码，让你自己写类似sllseg的东西。上届学长说特别简单，可能像c老师这种天才根本不知道我这种普通人的智商水平，随手加点难度就把我干懵了（我还以为我单子学得特透彻，ohno）。 7. 平时作业满分三分向下取整，放最后是因为这是槽点里最微不足道的一个。 本门课是我在交大上过体验最差的一门，如上所述，每个环节都揣着一个放到别的课能被冲烂的槽点，而伟大的c老师愣是集齐了一整套。哥们除了这门课核心学积分94+，这门课还是我花时间最多的一门，80出头的分数比我通识课都低。写coq大作业时只有深深的无力感，因为完全不知道到底咋做。 悲伤的是后面还会有一届届ieee cs的同学来坐这个大牢，再想想ieee cs的保研卷度（指硕士夏令营初筛卡小专业50%），ieee cs就是交大最烂cs，且看不到任何好转的希望。 本来是想骂人的，但把槽点列一遍已经耗尽我所有力气。 sb东西，nt课程 **Admitted.**

普通cs专业的 pl 方向专业课都已经停开2年了，ieeecs这边居然还把这玩意当必修供着呢😭

课程内容：编译原理 上课自由度：一般 考核标准：较高但给分很慷慨 授课质量：极高 期末卷子简单到接近白送，基本不犯猪脑子就能拿高分。平时作业分数向下取整，可最后折算总成绩的时候又慷慨得不行。大作业确实比较硬，听说隔壁写coq的已经写到心力交瘁…… 这确实是个问题：不同项目的大作业难度并不等价。一般来说，选coq会难很多。 不过我们选的是程序实践类，不碰理论证明，把要求的东西都搓出来基本也就只扣一个组队分。曹老师的大作业我个人觉得很舒服，要求清晰明了，给分明确，不卷报告不卷创新，虽然不好水但绝对公平公正。实践过程还能帮着消化平时讲的些理论，负担也不算重。 至于有的评论说课太难听不懂，额，我个人的感觉是曹老师的课程只要你听了，理解起来也没那么困难吧，很多东西确实得自己听了才有发言权。确实很难上课一遍听懂，基本每节课都要回放听，但能上课一遍听懂的课也没多少了嘛（）

课程内容： 是有点难，编译器、程序语言的指称语义这一堆 上课自由度： 自由得很，可惜内容量巨大，一节课掉线后面几周就属于天天追赶大部队 考核标准： 把Coq大作业撇开不聊，考试简直是easy档 授课质量： 高，质量是真的没得说 --- “本来想打低分，就冲这两个月COQ把我写的心力交瘁，可他给的分实在是太多了。。。” --

课程内容：从编译器实现的角度出发，前端语法词法分析一路干到后端寄存器分配等等都沾，曹老师的水平是真的高，甩我们几条街（这事是真的） 上课自由度：高，但平时分盯课堂发言和qq群发言，跟助教私发的大概也算数 考核标准：期末25%，大作业25%，平时作业40%，平时分10% 授课质量：唯一可能不太合适的地方就是塞了太多coq验证，对不做程序语言形式验证的人来说基本是买了台跑步机回家挂衣服。要多讲讲编译器代码实现可能对cs同学更友好、更对胃口。如果你写过完整的编译器项目，尤其是高质量实现，掺没掺编译优化都算加分，面试或申请时很有用。

出分后最后追评一条：期末考那难度可以说是低到地板上，最终给分也是相当大方；志在冲A+的同学课上最好多刷点脸熟，不然就会像笔者一样，最后控分的时候课堂参与分这一块儿只能干瞪眼 --- 在剩余一个引理的某个分支里还有一处压根没证的情况下，我们这组的最终码量落在11000行左右... ---- ## 21级Coq的大作业预估平均码量在5000行以上 GPT救不了你，网上你也查不到任何你要的资料，除了凌晨跟cqx对线、祈祷他大发慈悲多吐点提示之外，已经无路可走；队友连续一个月把这鬼东西写到凌晨2-3点；一个月Github commit了300+次；期末周考一半隔壁OS一个字没看还要接着肝这坨东西... --- 贴两个链接给诸君赶作业的时候乐一乐 曹大师的知乎主页：https://www.zhihu.com/people/qinxiang-cao/answers 着实有资格特立独行：https://tieba.baidu.com/p/525509323?red_tag=2829944032 ——**“我签的是北大，不是清华！”** --- 你说得对，但是一次作业3分直接折算总成绩，每道题全对或全错而且总分下取整。国庆假期布置一份3分的编程作业，工作量比隔壁操作系统一整个lab还猛，花上两三天被Flex和Bison反复摩擦，还可能因为隐藏样例不过就直接得0分（**像过去CS1601或者其它课那样设个2/3的保底分有这么难吗，哪有平时作业认认真真写三天还敢给你打个0分的操作啊**）。 平时都已经是这德性了，参考前面学长学姐的评论，大作业是真不敢想象。建议兄弟们平时作业就抱着Github上CS2612前辈们的经验过河，可叹这种nt的lab居然是某些人今年新想出来的。 都是IEEE CS的人嘛，按说不算太蠢，天天被这种评分体系、还有跟绝大多数人科研方向八竿子打不着的作业来回折磨，我想这锅应该也不全该我们背。 给2分是因为课确实是用心上的，cqx老师作为高中阶段信息学加数学的双料金牌，是同时被保送清北的存在，水平当然没得挑。但除这以外的所有东西，都让人贼痛苦，也完全看不到哪一天会好转。

课上得还算能听吧。。不得不承认这哥们脑子是真转得快。但你要是凑上去跟他本人掰扯问题，有时候那压迫感直接拉满（尤其是他脸色不好的时候），空气都能给你冻住。 劝退他的实验室，进去约等于自费解锁"免费劳动力"成就（别被竞赛光环闪瞎眼），c老师在这一点上属于人精级别。真对PL上头、想润出国，可以早点去勾搭暑研/实习；不打算润的话，还是尽量往热门方向凑，Coq定理证明在国内基本属于冷宫技能。在cqx这儿主打一个帮他写Coq证明，功利点算账的话，paper署名、拿得出手的项目、PL知识这些，收获都少得可怜。

难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难难 混子人士的处刑场

我尽量从普通学生的坑位里，给本学期这门课来个不吹不黑的客观评价，纯路人视角，不搞神仙下凡。 首先，从课程内容来说，课程网站传送门在[课程网站](https://jhc.sjtu.edu.cn/public/courses/CS2612/)。本学期把Coq定理证明器请来当教学辅助工具，基于While语言讲了词法分析器、语法分析器，还实现了一个简单解释器；紧接着三个比较重点和难点的章节闪亮登场：指称语义、霍尔逻辑和小步语义，属于脑内CPU开始啸叫区；最后是基于While语言的简单编译器实现，以及函数调用（其实最后两节课还夹带了一些lambda表达式，但是考试不要求，像彩蛋但不算DLC）。总体来说，这门课的课程内容大体符合PL方向入门的要求，除了Coq定理证明器的理解和使用让人比较捉急（特别是一些语法，建议用专门的习题课来讲解），其余课程内容还是能够提高我本人的离散数学和逻辑学素养。 第二，从老师的备课、讲课情况评价一下。本课程较为抽象，比较难懂，且本学期是第一次改为中文讲义，老师可能也是同时准备两门课，所以同学们基本上没法在课前获得slides或者讲义，直接导致课前没法进行一定量的预习（对于类似的课我的感觉是预习挺重要），听课也就云里雾里。再提一下老师的讲课，老师水平还是很高，但可能有时没有顾及到同学们的接受程度；虽然课上经常询问是否有问题，但许多同学反映，实际上是因为从头就没听懂所以提不出问题。希望老师能够放慢速度，适当复习，减少一些较为困难复杂的内容。 第三，从课程的各项安排上评价一下。评分分为四项：平时分10（看课堂发言、群聊发言等），作业分45（难拿），大作业20（有点难拿），考试25（这次考试较简单）。老师的作业有好几种，有时是手写的选择、判断、或者证明题（推荐用Markdown或LaTeX写），有时是Coq证明题（较简单），有时是编程题（词法分析器、语法分析器、简单解释器，简单编译器）。作业部分的手写证明题较难，经常失分，作业扣分挺重，直接等比例折算**向上取整**计入总成绩。大作业选题挺关键，一般Coq证明题较难，写编译器或者解释器简单一些。总结一下，老师被吐槽比较多的主要是作业的给分：有时一点点错误就导致3分一次的作业变成2分，有时错两三点甚至只有1分，导致做作业压力挺大，像背着锅在雷区蹦迪。 最后，我想总结一下：老师准备的课程内容还是不错的，但是还需要多考虑同学们的接受程度（我本人是每一堂课都要听回放，再自己琢磨，回放都快盘出包浆了），希望老师能把这门课开得更好！

课程内容： 上课自由度： 高，像没人管的自习课 考核标准： 严得像个强迫症的精神病患者。有一点错误，三分的作业最多给两分，再错一点直接一分，给分只给整数，半对就是错，意思思路对了但写有瑕疵也算错。助教argue从来没成功过，最后作业分向下取整，总评再向下取整。 大作业巨TM难，属于把你当逻辑大师兼coq高手来练，丝毫不考虑大作业的难度远高于学生的脑子和精力，也丝毫不考虑学生实际的coq编程水平。 授课质量： 如果说喝一口水就再也听不懂老师讲的东西叫高质量授课，那么这授课质量嘎嘎高。 总结： 如果CS不是必修这门课，我直接中期退课，sb课程安排，变态课程要求，主打一个让人破防。

课程内容：满分五边形战士。 上课自由度：5 考核标准：5 授课质量：5，一段沉默的五连全垒打。

本片包含以下要素： Coq但是Admitted，代码界的薛定谔的证明，写没写都算数；《向下取整》，分数像滑梯一样只往下滑；《你这是关键步骤，不是显然》，但对我来说全是不显然；上课笔掉了去捡笔，然后啥也听不懂了，一支笔引发的学术跳水。 考核标准： Lemma 考核内容=(15次作业/\大作业/\期末/\课堂表现) /\ 考核标准=你就等着寄吧： intros. try tauto. try auto. (* 我啥也证不出来啊 *) Admitted.

Abort得比我凌晨三点的编译梦想还干脆。（* 凭啥推荐指数这评分卡从1起跳，0这个键是被教务处吞了吗？*）

Lemma 我没寄:   完成 大作业. Proof. Admitted. (* 这波啊，这波是直接缴械投降，Coq 看了都想给你颁个"已读不回"奖 *) Lemma FALSE:   False. Proof.   pose proof 我没寄.   tauto. Qed.

讲课凑合，难度高，标准严，压迫感极强，坐教室里跟在老板工位摸鱼似的； 大作业强制每组不同题，难度大且题间难度差异大，纯靠抢，堪比双十一零点火拼手速； 所有成绩向下取整，argue分数基本无效，申诉系统仿佛是心理安慰摆件。 总体而言，老师对课程是用了心的，但对学生能力、课程难度、实用性的考虑十分欠妥，对作业及评分的标准和策略毫无温度，整体体验不佳，有种在难度和压迫感的夹缝里走钢丝的感觉。

课程内容：Admit——拿编译原理当背景板，一上来就是先放你进门，别问，问就是能被录进来算你赢 上课自由度：Auto——这课自由度跟自动挡似的，你挂不挂挡它都自己往前冲，反正你要做的只有别翻车 考核标准：Contradiction——前半句说我听懂了，后半句说这也能算懂？标准在你脑子里原地打结，跟编译器报错一样谁也说不清谁对 授课质量：Qed——证完了，就这么回事，你要非让我再补一句也只能说确实证完了