SOSP'24 - 第三天

还坐在会场，先写几句怕忘记了。

这次开会的一点感受是，首先耳朵不好使了，别人说话的默认音量对我来说有点清不清楚；然后是脑子不好使了，听到英语就像背景噪音一样，哗啦哗啦的不知道在说啥。使使劲认真听，还是哗啦哗啦的。

也许我出来开会就是会比其他人的体验更负面一点，这是由我的叶公好龙导致的。对于会议上入选的大部分工作，我都会有些许的熟悉，会在背景介绍的部分希望能有个跳过过场的按钮。从而，会不自量力地觉得这玩意为什么就不能是我做出来的呢。然而拥有做出一个工作的原料距离把一个工作制作出来还远之又远。我不懂得这个道理，又广泛地收集了各种工作的原料，我不低落谁低落。

我的科研直觉，或者说下意识的想法，还是不够好。上午听到针对代码即设施（IaC）的验证工作的时候，（在心里暗自）捶胸顿足这是一个我多么熟悉的问题。为什么我没有想到要去做个工作呢？因为我满心都想着，并自满于自己多么有能力去解决这些问题了，压根没想过要做个工作让（不管有没有能力的）别人都可以不用解决这些问题。

个人能力也许会对科研的敏锐度产生影响。更准确地说，是个人能力所带来的傲慢。抑或说，傲慢总是不可取的。

昨天中午偶遇了Josh，但是没聊。不知道走之前还有没有机会跟他聊几句。

---

坐在登机口了，会议最后一天的太阳即将沉入夜色。

写完瞅了一眼前面写的。最后也没有找到Josh就走了。

吃了一顿没有novelty的晚饭，买了两个造型怪异的玩偶。我做的选择向来都很差，平时都不太在意，只是在这个情境下还是对此有些不舒服。

今天逮着Verus老哥聊了几句模型检查，然后发现人家并不熟模型检查。

大体上有个对基于异步语法和结构化并行范式编写的Rust程序做模型检查的点子。不够清晰还不足以写一篇内容出来。

我问他，你觉得有哪些部分的场景会是那种落入Rust的舒适区但是没有落入Verus的舒适区的（也即更适合用模型检查去做的）。他旁边的小伙伴，呃，老伙计说，那种写几句就撂下一句断言的感觉会是这样的。

另外还找昨天给JavaScript的JIT编译做验证的作者聊了一下。称赞了她的幻灯片。昨天还有几个幻灯片我也想当面称赞一下，就是已经记不得作者长什么样了。

向她讨教做幻灯片的经验。她上来就说我是拿Google Slides做的，我当场放弃。人家这是纯粹的天赋，学不来。

她说一开始就要把所有的预设全去掉，然后按照UI设计的思想自己鼓捣一套出来。我说你说得对。

---

感觉以后都不出来开会了吧。

除了发出去了要讲的话，就是陪𝒦去这样子。我现在大概是没有本事陪的，不知道之后要怎么才能有这个本事。