编程语言入坑指南

本文先按照理论和应用两方面介绍了编程语言方向的相关概念，而后介绍了清华软院静态分析组研究的内容。最后本文介绍了该方向的科研就业现状，并给学弟学妹们给出一些建议。

作者介绍

我叫孙子平，是：

• 软院五字班本科毕业生
• 软院零字班工学硕士在读

主攻静态分析方向。我的微信ID同GitHub ID，欢迎大家通过微信、邮件私戳，相关联系方式见页面下方名信片。这篇文章大多是原创的个人观点，仅供参考，也欢迎来评论区指正。

编程语言方向简介

早在高中时，我就萌发了一个梦想，希望能参与到知名编程语言的设计中。当时，我认为那是编程领域的圣杯，是一个值得毕生奋斗的目标。进入大三后，我依旧怀揣着这个梦想，只是这个梦想具化为了一个领域，编程语言领域。大家通常简称它为PL（Programming Language）。当时，我找到了Paul Zhu学长。他告诉我软院与PL最相关的方向可能是：

1. 周旻老师的静态分析方向；
2. 贺飞老师的形式化验证方向。

恰巧当时我很喜欢函数式编程课，讲师理论上是周老师。于是，我联系了周老师，成功入坑静态分析。这门课程后来被取消掉了，也算是很遗憾。

PL主要研究编程语言的设计和实现。它的一方面很理论，包括形式语言与自动机、类型系统；另一方面则偏应用，包括编译器和静态分析。接下来，我讲按这两部分介绍一下PL，希望能够激起有兴趣的人对此的热爱。

PL理论篇

编程语言相关的理论有很多，这里我选取两个较为典型的理论体系：形式语言与自动机，和类型系统。我会更偏重于后者，因为前者是软院已有的课程。

形式语言与自动机

形式语言与自动机是软院大三上的课程。这一系列的理论试图将现实世界中的计算，抽象为一个可以用数学描述的行为，从而进一步描述计算能力和计算复杂度。这些理论发展得非常成熟。到了现代，容易摘得的科研果实基本已被摘取，只剩下一些非常难啃的硬骨头。在这些硬骨头中，最著名的应当是P/NP问题，其难度不言自喻。有趣的是，形式语言与自动机理论也能用于实现编译器的前端。

类型系统

相较而言，类型系统则更能激发我的兴趣。编程语言借助类型检查，可以限制所能进行的操作。根据这种检查发生于编译期还是运行期，类型系统可以分为静态的和动态的。而根据其对隐式类型转换的允许程度，可以将类型系统划分为强类型和弱类型。

类型之间的关系则更为有趣精妙。以下部分大多是个人观点。多态，是指不同类型在同一代码下拥有不同的行为。其目的是提高代码复用能力。面向对象最具吸引力的特性正是多态。相较之下，封装很容易实现，即使实现了也只是“基于对象“，谈不上“面向对象”；而继承的目的则要么是组合（Mixin），要么就是多态。面向对象强调的是动态多态，即在运行时才决定何种行为。类似地，也有静态多态，即在编译期就决定何种行为。例如，二元加法运算符作用于数值类型时表现为加法，作用于字符串类型时表现为拼接，这就是静态多态；函数重载也是静态多态；而类似于C++的模板泛型编程，则是更为强大的静态多态。更多安全的、符合直觉的多态意味着更高效地复用。举个例子，考虑下面的几种操作：

• 拼接字符串数组
• 求整数数组的最小值
• 求二叉搜索树上所有浮点数的积

这些操作都是针对一个可以按某种顺序遍历的容器，将其元素按照某个有单位元且符合结合律的二元操作收集起来。在C语言的时代，人们很难想象这些操作能用统一的代码完成。而借助多态，这种程度的代码复用就成为了现实。例如C++中，你可以用std::accumulate做到上面的所有操作。

#include <iostream>
#include <vector>
#include <string>
#include <numeric>
#include <set>
#include <limits>

using namespace std;

int main() {
    vector<string> strings { "hello", " ", "world" };
    vector<int> doubles { 3, 1, 2 };
    set<double> ints { 2.0, 3.0, 0.1 };
    cout << accumulate(strings.begin(), strings.end(), string(), plus()) << endl;
    cout << accumulate(doubles.begin(), doubles.end(),
                       numeric_limits<int>::infinity(),
                       [](auto a, auto b) { return min(a, b); }) << endl;
    cout << accumulate(ints.begin(), ints.end(), 1.0, multiplies()) << endl;
    return 0;
}

而有些函数式语言，则将多态的技能树点满，并配之以简洁的语法，构造出令人惊奇的代码。

import Data.Foldable
import Data.Monoid
import Data.Semigroup
import qualified Data.Set as S

main :: IO ()
main = do
  print . fold $ ["hello", " ", "world"]
  print . getMin . foldMap Min $ [3 :: Int, 1, 2]
  print . getProduct . foldMap Product $ S.fromList [2.0 :: Double, 3.0, 0.1]

从上面的描述中，可以看出类型系统不仅能确保安全。它更是编程语言实现代码复用的利器。它是编程语言千篇一律的语法词法下，有趣的灵魂。然而类型系统不止于次。Curry-Howard同构指出，命题与类型有着对应关系。而命题的证明则对应于类型实例的构造。自此，类型论成为了集合论的竞争者，并成为了计算机辅助证明系统主流实现的基石。举个例子，下面是一些常见的命题和类型的对应关系。

因而，为了证明下面的逻辑命题

$$(P\rightarrow Q) \rightarrow (\neg Q \rightarrow \neg P)$$

即

$$(P\rightarrow Q) \rightarrow ((Q \rightarrow \bot) \rightarrow (P \rightarrow \bot))$$

在类型论中，可以构造下面的solution函数：

from typing import Callable, TypeVar, NoReturn

P = TypeVar('P')
Q = TypeVar('Q')

class Never:
    def __init__(self) -> None:
        assert False


def solution(f: Callable[[P], Q]) -> Callable[[Callable[[Q], Never]], Callable[[P], Never]]:
    def foo(g: Callable[[Q], Never]) -> Callable[[P], Never]:
        def bar(x: P) -> Never:
            return g(f(x))
        return bar
    return foo

你可以把这段程序丢给Python的类型检查工具mypy --strict，检查一下所有的类型注解是否正确。mypy通过类型检查就验证了上面的证明是正确的。这使得基于类型论的辅助证明系统能够永不会失误地验证证明的正确性。想象一下在未来，某个数学家给出了黎曼猜想的证明。那是一份长长的代码。全球的数学家们把代码输入进计算机辅助证明系统，就可以立刻判断这个证明的正确性。

当然啦，没多少人用Python做计算机辅助证明。下面是使用Coq定理证明器证明上述定理的代码

Theorem example : forall P Q : Prop, (P -> Q) -> (~Q -> ~P).
Proof.
    intros P Q f g.
    exact (fun (x: P) => g (f x)).
Qed.

总结一下，类型系统对编程语言影响深远。类型的约束能过确保程序安全；类型系统的表达能力则关系着语言的抽象、复用能力。而类型论则能使编程语言成为数学定理证明的工具。

PL实战篇

编译器是指将源代码翻译为可执行程序的软件。静态分析则是指在不运行程序的情况下寻找代码的漏洞。像JetBrains全家桶和VS Code插件们的一大卖点就是快速且强大的静态分析能力。编译器与静态分析对编程语言的实现而言都至关重要。

编译器

编译器的书大多会花很多篇幅讲如何实现编译器的前端，也就是如何解析源代码。其实我个人认为这有点舍本逐末。如果你要设计的语言是上下文无关文法，那么Yacc、ANTLR之类的工具就非常合适。然而不少语言无法简单地用这类工具解析。它们大都上下文相关。C++里

int main() {
    vector<string> array;
}

那对尖括号看上去像是模板参数列表，但实际上，搭配下面的上下文，就成了大于小于号。

#include <iostream>

struct {
    int operator < (int other) {
        std::cout << "hello, world!" << std::endl;
        return 0;
    }
} vector;
int string = 0, array = 0;

C语言的A * b;也是经典的二义性语句。根据A为类型还是变量，它可能是指针定义语句，也可能是乘法的表达式语句。针对这些非常复杂的上下文，手写递归下降是我最推荐的解决方案。实际上主流的编译器大多是这样解析源代码的。

编译器相对更重要的部分是设计中间表示，并在之上优化。这部分的知识会非常琐碎，就不多介绍了。对于要做编译原理大作业的同学，可以参考计算机系的MiniDecaf 编译器结构。值得一提的是，来自苹果的LLVM已经成为了现代编译型编程语言实现的首选基础设施。

静态分析

在我眼里，静态分析是很现实的。由于图灵机糟糕的性质，静态分析试图解决的所有问题都几乎是不可判定的，包括被解引用的指针是否为空、数组是否越界、除数是否为零。这就会导致静态分析是个工程问题。

我们组在静态分析上的研究内容主要有两部分：

• C语言上基于LLVM的值流分析
• Java上的污点传播分析

前者是用值流图建模程序。图的节点是值，而边则从值的定义指向值的使用。类似于空指针解引用等的缺陷挖掘，也就被转化为图上的路径搜索。后者主要用于查找SQL注入之类的漏洞。它将Web请求的输入视作被污染的数据。如果被污染的数据未经清洗（例如转义）就传播到了重要的调用（例如数据库命令），就被视为一个漏洞。

现状与建议

科研

编程语言各个分支的研究都较为成熟。很多时候，我都在阅读上世纪的文献。这使得新的发现变得更加困难。所以对于真的想发论文的小伙伴，这个方向是比较硬核的。

就业

编程语言的应用方向一直不温不火。伴随着AI芯片的火热，这方面也确实有编译器人才缺口。但总的而言，国内需要编译器人才的公司非常少，主要是华为等一些带有民族色彩的企业。外企的话，像微软、Intel都一直有这方面的人才需求。如果你很喜欢这个领域，那这里的就业也不会让你很失望。

结语

我个人认为编程语言领域是非常有趣的，它的很多方面都吸引着我继续探索。然而，这一方向的研究有一定难度，主要是其本身发展较为成熟。就业方面，编译器的就业需求和供给都是较为稳定的，不会出现太多问题。