郭旭东 Cloud Native Community
虽然多次接受采访，但是采访别人这还是头一遭。今年的 7 月初，我参加了公司举办的《极狐 GitLab 中国行成都站》活动，在活动中认识了一群对于编程非常有热情的在校大学生。他们标准的 00 后，但有人接触编程的时间比我还要长！而其中一位自称 千里冰封 的小伙子吸引了我的注意，让我有了做一期专访的冲动，当时他大三休学（发稿时他已经回到了学校继续完成他的学业），大一曾在 PingCAP，大二则在 JetBrains 实习，对于编程有自己非常独到的理解和认识。
我平时工作比较繁忙，而他又在国外求学，以及时差等因素，几经波折我们才完成了本次专访，我惊讶于他丰富的编程经历的同时，也从他的经历中学到了很多我个人缺乏的东西。
Q：先和大家介绍一下自己吧？
千里冰封：采访前，我拿到的采访提纲里，标题写着 「00 后」 「大二 JetBrains」 这些吸引眼球的标签，我个人不是很喜欢这样（我更希望别人能关注我自己的研究方向和作品，而不是我的个人经历），就把标题改的简单了一些。（编者注：没错，我又把标题改回来了 ㄟ(▔▽▔)ㄏ ）但是这些都是真的：我是一名 00 后编程爱好者，因为休学一学期导致今年依然在读本科大三，在成都生活到 18 岁后在 Penn State 就读，位于宾夕法尼亚州的城市「State College」。目前因为个人兴趣，打算从事一些计算机方面的科研工作，方向是技术上的编程语言理论、编程工具链设计方面，以及数学上的几何拓扑方面。
Q：是何时开始接触编程与开源的？
千里冰封：严格来说是初三毕业前夕，所以我一般对外声称我是高一开始接触编程的。我高中就读于成都外国语，是两位类似领域里的大手子的学弟，而我正式开始沉迷编程是初三的本校直升考试前夕，这使得我的父母非常反对我编程（和大部分国内父母反对子女打游戏一个道理：见不得子女沉迷考试之外的东西）。这种反对持续到了我高中申请结束前。我准备了一年半高考，但是因为成绩不好加上种种原因转而走向出国的道路。托福和 SAT 加起来准备了半年，再加上准备的时候也沉迷编程、不务正业，最终成绩也不算理想，申请遭到「连环拒」，这也导致我对给我发 offer 的学校心怀感激——即使我在这里并没有找到专业对口的教授。
接触编程是因为初中的时候对电路感兴趣（受外公影响）。我在听说了电路的行为可以直接通过计算机来「烧录」改写后，就一心想学习怎么给集成电路写程序。我在网上查啊查，搜到了 『C 语言』 这个关键词，然后顺藤摸瓜继续搜索，先后看了《啊哈 C》（网上免费版只能阅读到 scanf 的章节，写出了能输入输出的程序后就要给钱了，而我当时根本没有钱）和『网易云课堂』上的某个免费的 C 语言入门课。限于当时了解信息的渠道，我只有这些资源来获取知识了。接触了软件之后，就永远地离开了电子电路，因为编程实在是太有意思了。在自学的过程中，我也掌握了熟练使用搜索引擎的能力，这对于一个现代的技术人员来说是不可或缺的关键能力，是本科计算机教育所不能教授的。
现在看来，入门时候了解的那些编程语言与知识对于理解编程和编程语言的帮助并不大，学到的知识又简单又过时（C 语言课用的 GUI 库都没装起来，Java 课推荐的 IDE 是 Eclipse），但是我当时对这些新奇的事物感到兴奋极了。但这些课程也不是一无是处，它们让我理解了一些内存方面的知识，这是当下流行的 Python 培训班所不能教授的。
Q：喜欢编程吗？为什么喜欢？
千里冰封：非常喜欢，喜欢到我不需要赚钱的时候也会以编程为乐。我觉得这种兴趣的产生可能和我的家人有关。我常年和母亲一起生活，她是一个拒绝逻辑思维、感性驱动的人，这间接使得我对这种纯逻辑性的创作方式有生理性的好感。直接原因大概是我喜欢思考吧——在编程这个领域中，不思考的人就会被淘汰、会写出令人厌恶的代码，所以我喜欢这个领域，它把我讨厌的人拒之门外。
近年来，在对编程语言和范畴论的学习中，我不断地发现有趣的、过去的我无法观察到的现象。这给人成长的感觉：如果我学编程学到一个程度就开始停留在输出知识的层面上，那我会感到很空虚，而如果我一直学习，就会感觉我在活着。比如我最近发现编程语言的「参数性（parametricity）」、类型宇宙的归纳与否和范畴模型里部分万有对象之间的唯一同构之间是有关系的，而我高中初次听说 F 类型系统和所谓参数性的时候，并不理解这个性质的重要性，查资料的时候看到就跳过了。
Q：能讲讲你在 PingCAP 和 JetBrains 的经历吗？你觉得在 PingCAP 和 JetBrains 都学到了什么？
千里冰封：按时间顺序来吧。我上大学之前在源伞科技实习，现在这个公司已经被蚂蚁收购了。当时老板说不能远程工作，而我上大学要去 A 国，正好机缘巧合之下，一位神秘的朋友把我介绍给了 PingCAP（下称「P 社」）的 CTO，然后就开始了一年的远程实习。
我很庆幸自己获得了在 P 社学习的机会，公司内部资料相对开放，我一个小小的实习生也可以阅读很多数据库业务、分布式系统方面的材料，这使我大开眼界。这一点上 JetBrains 也是如此。我的实习 mentor 说话声音很好听，定位内存泄漏（肉眼阅读代码并查找问题）也很快，我很喜欢他。但是因为我是远程工作，时差十二小时，在公司内部很缺乏社交，来来回回也就认识了 TiKV 组的几个同事，颇为遗憾。我在职期间正好碰上「将 TiKV 捐赠给 CNCF」这一事件，同事们为了这件事都忙得不可开交。希望事后他们得到了足够的休息。
我认为 PingCAP 很懂程序员心理（离职后才知道有很多事情是彦青做的，比如 P 社周边玩具、饰品等），而且还把开源社区经营得欣欣向荣，吸引了很多外部贡献者。但是我不是很理解为什么他们坚持在部分 TiDB 的子项目上使用 Go 语言，简直污染了整个生态。
关于在 JetBrains 的经历，一言蔽之，体验是非常不错的。我的技能和同事、导师是互补的，他们可以在类型论、范畴论上指导我，而我则对 Gradle 之类的工具比较熟悉，可以帮他们写一些他们整的不太好的东西（之前他们在构建脚本里面删目录，这个操作我看到都惊呆了）。更多的内容可以参考这个回答。写的不算很正式，但也算是我的肺腑之言，而且褒贬共存，视角是比较客观的。
Q：都参与过哪些项目？
千里冰封：个人的话写过四五个 IntelliJ IDEA 的插件，大部分现在都不再维护了。比较有趣的两个是，一个是 Pest 插件，一个是 DTLC 插件。前者支持了 Rust 语言的一个语法解析器生成器，并且内置了这个 Pest 编译器本身。这个技术是通过将编译器（使用 Rust 编写）编译成 Web Assembly，然后再用一个开源项目把它进一步编译成 Java 字节码，最后再在 IDE 里面加载实现的。对接生成的代码时，可以清晰地感受到 Web Assembly 的内存模型。后者支持了大于 10 个实验性编程语言，我通过代码生成实现了大部分语言的大部分功能。通过这个项目，我验证了自己曾经关于「像自动生成语法解析器一样自动生成 IDE」的想法，但是这个想法已经被先行者快人一步更彻底地实现了。除此之外，我还用 Rust 复刻过一些类型检查器、用 Java+JNI 糊了一个 dear imgui 的 Java 绑定、用 Kotlin 编译器内部的 IntelliJ IDEA 内核做过一个性能极差、功能不全的微型 Kotlin IDE，支持插件加载（我给这个小型 IDE 写了接近 10 个插件，基本上可以通过提取并修改 IntelliJ 插件的源码实现）。
目前我在 PLCT 实验室组织了一个团队，主力开发一个定理证明器「Aya」，招聘贴和相关链接在这里。我很憧憬我现在的老板，他是一个很有魅力的人。
在公司的话，我觉得值得一提的就是在 JetBrains 参与开发的 Arend 定理证明器的套件，包括编译器、IDE 插件和数学标准库。代码在 GitHub 上搜「JetBrains Arend」就可以搜到了。
Q：都使用哪些编程语言？最喜欢的编程语言是什么？
千里冰封：最近使用 Java 17、Haskell、Agda、Rust 等语言编程、使用 JavaScript 完成物理作业、使用 Haskell 完成（部分）数学作业、使用 TypeScript 开发 VSCode 插件、使用 Kotlin 开发 IntelliJ 插件。没有特别喜欢的编程语言。
对我来说，实用编程语言分为两种，一种是依值类型系统的编程语言，这些语言基本上都很难用。剩下的编程语言的类型系统对我来说都是一样的，那么就工具链和编程体验而言我觉得 Java 17 在这些语言中是最好的（有模式匹配和代数数据类型，代码补全、浏览代码、生态、执行性能、调试等都不错）。
如果不考虑「最近」这个因素的话，从高中开始，用过的语言我已经数不过来了。为了学习编程语言的理论而不得不学习了很多我并不感兴趣的编程语言，这些语言看完一些基本思想后就丢掉了。
Q：目前正在关注哪个领域？可以推荐一些你喜欢的开源项目吗？
千里冰封：在关注定理证明器、编程语言理论、类型系统等领域。我很高兴自己（目前）有足够的智力和恒心跟进类型的理论在近年的发展。不论是类型理论的设计还是实现，在近几年都有非常突破性的进步。追随拓荒者的脚步探索未知领域是一件美妙的事情。
Q：毕业后希望做什么？对未来发展的期望是什么？
千里冰封：如果申请顺利就读博，不顺利就找工作。希望自己能赚到钱、学术生涯不要太坎坷。
千里冰封只是广大 00 后开发者中的一员，有更多像他一样从小接触编程、热爱编程的人已经开始进入职场成为我们的同事和朋友。在开源社区中也结识了不少 00 后的开发者，他们有热情、有想法、有能力，如果能和他们一起共事，我将非常开心。也希望千里冰封能顺利完成他的学业，在学术界能有一番作为。