我第一次听说 Coq 是在本科的时候。从那以后我就一直很想学 Coq，但是并不知道怎么开始。大部分的 Coq 教程都是在讲逻辑，我觉得并不是很有趣。

上个学期我选了 UW CSE505 这门课。Prof. Zach Tatlock 和 TA Talia Ringer 设计了一系列非常棒的作业来帮我们学习 Coq。在这个课里面，我们证明了一些更加实际的东西，包括一个简单的编程语言的解释器还有一个简单的正则表达式引擎。事实上，我发现我对在 Coq 里面写证明还蛮在行的（但是写规范就完全是另外一回事了），至少在做作业的时候我是这么觉得的。

如果你在自学 Coq，我推荐以下资源：

• UW CSE505 的作业
• Formal Reasoning About Programs 这本书是我们上课的教材。这本书很短，边距很大，空白很多，每一章附带了详细的 Coq 代码。这本书还自带了一个很好用的 Coq 库 frap。
• Software Foundations 如果你真的对形式化验证很感兴趣的话。

我非常高兴我终于能把 Coq 从我的愿望单里面划掉了。不过我并不是形式化验证的狂热粉丝，我觉得我之后也不用用到 Coq。我决定趁我还没完全忘记 Coq，赶紧把我做作业时学会的 Coq 技巧写下来，万一以后哪天我又用到 Coq 了呢，希望也对读者有所帮助。

这算是开了 CS140e 的坑了吧。在淘宝上买树莓派的时候发现了出了3B+版本，而课程用的是3B版本。新的性能要强得多，肯定要买新的呀。但是，3B的CPU是BCM2837，3B+的是BCM2837B0，买的时候有点担心能不能正常地运行 CS140e 的程序。

收了货试了下，果然不行。ACT灯先慢闪4下再快闪4下，循环往复。搜索 raspberry pi act led，找到了这么一个wiki，上面说闪4下是 start.elf 无法载入。

我猜测这个 start.elf 可能不是课程专用的，于是搜索 start.elf raspberry pi 3 “b+”，找到了这个帖子，发现了官方的固件，用里面的 start.elf 替换就能成功启动了！

“放大放大再放大，每一根毛都看的清清楚楚。”

——[欢乐笔记本]内置病毒AIPC笔记本电脑

前些天我在写毕业论文，自然免不了作图。我相信有很多读者像我一样有这样的强迫症：插图不是矢量图就浑身难受。插矢量图的好处都有啥？

• 放大看也不会模糊
• 可选中图片中的文字（似乎也没啥用）
• 看起来更像是自己画的而不是从网上截图

LaTeX 作矢量图的一大流派是 tikz，但是这个包对我来说还是太难了，总是学不会。而且我总是觉得，作图这种事情，就应该是在图形化界面里面拖拖点点更加直观清晰。之前我也听说有人用 InkScape、Ipe 等等软件的，但试了一下用起来总是不顺手。

可能是因为做幻灯片的机会比作图多得多吧，我发现我对 Keynote 非常习惯，于是理所当然地，我就顺带用 Keynote 来作图了。下面就介绍一下我在 macOS 下面作矢量图的经验，里面也包含了一部分用来做幻灯片的技巧。

PUBG？是的就是你正在玩的《绝地求生：大逃杀》。

“挖矿”？蓝洞也出区块链骗钱了？呵呵，不是的呢亲。

TLDR: 自己还是太年轻，赚钱的机会千千万，只是当自己意识到的时候已经错过了末班车。所以啊，还是要提升自己的姿势水平。

让我们来看看下面这个简单的代码：