9.11

社会实践

为了通过 “新时代社会实践” 课程，去中共一大会址进行了 “社会实践”，实际上就是拍了 10 张照片和一段口号视频来满足提交材料的要求。

细节懒得写了，开摆。

心有灵犀

社会实践结束，骑车从地铁站前往校门的过程中，恰巧遇到曹钦翔教授对向骑来。我不知道他还是否记得我，但我一定忘不了这位在转专业面试时有过一面之缘的神一般的人物，个人主页上的 1st place of NOI 2008，1st place of CMO 2009，已经不是人类了！

回宿舍后，搜到了一篇他指导的 PRP 论文 实数的康托尔构造理论在 Coq 中的形式化，学生名叫周李韬，和他一样，都是上中毕业，完成这个 PRP 的时间是大一下。最重要的是，PRP 的选题正是我在了解 Coq 后想要干的事——用 Coq 把《陶哲轩实分析》里的基于柯西列的实数构造写一遍！这就是跨越 6 年的知己啊！

根据 个人主页 可知，周学长在 HKU PL Group 读 phD，已经一作发了 3 篇 POPL，1 篇 OOPSLA，大概也是 PL 科研天花板级别了吧，此等强者，我又怎么好意思说是知己？只能仰望了！

跑

今天又提升了一点速度，明天继续！

北大未名 BBS

在水源上看了不少就业分享贴，好奇清北佬的就业情况怎么样，顺便为了观察一下其他学校的论坛氛围，于是搞到了一个北大未名 BBS 账号一探究竟（这个账号可以通过 THU, PKU 和 RUC 的邮箱注册，感谢来自 RUC 的账号支持👍）

进了论坛，发现相比水源社区，这里冷清得过分。 帖子很少；常常有帖子无人回复；没有长久更新的日记帖；用户平均年龄更大；没人整活；没有趣图楼；没有水楼（甚至闲聊的话题都很少见）；鹊桥帖没有勾勾叉叉；没有贴表情功能。这些侧面当然还难以完全体现那种进入论坛后巨大的落差感。最终，也没有任何什么就业经验分享贴。在未名 BBS 搜索 “Coq”，调整时间范围到最大 1000 天，没有任何结果；但在水源社区搜索 “Coq”，有 58 个结果。难道北大还有其他神秘论坛吗？北大的学生在哪里讨论学问和技术呢？

我不知道这是怎么回事。

总结：北大 BBS 半死不活，清华和复旦没有论坛，只有树洞，浙的 CC98 没机会进去看。交又赢！😀