每天写代码时，我们很少追问一门语言为什么拥有这样的语法、一个表达式怎样获得意义，或者两段程序在什么条件下可以被认为等价。程序语言理论把这些习以为常的问题重新摆到桌面上，并尝试用一套可推理的结构回答它们。
这个系列先从不同语言范式的全景开始，随后借助一个足够小、却能表达关键概念的模型语言 PCF，逐步介绍语法、语义、递归、类型与证明系统。最后两篇把视野扩展到代数数据类型和命令式程序。阅读它并不要求你已经会设计语言；熟悉基本编程概念，就可以从第一站出发。
模型语言看起来远没有现实语言丰富，这恰恰是它的价值：去掉工程细节以后，语法、类型与计算之间的关系会变得更容易观察。
十一篇文章
先看全景：程序语言有哪些不同家族？
从命令式、函数式与逻辑式风格出发，观察语言设计的不同选择。
从模型语言和 Lambda 记号开始
认识抽象、应用、作用域，以及公理语义、操作语义和指称语义的基本视角。
读懂文法、逻辑与归纳证明
补齐后续定义需要的数学语言，包括文法、不同层次的逻辑和证明系统。
PCF 的语法：类型、项与函数
区分对象语言与元语言，并建立 PCF 类型和表达式的基本结构。
同一段程序，可以怎样解释？
并排理解公理语义、操作语义与指称语义，以及它们刻画的程序等价关系。
从记录与元组走向迭代和递归
理解语言结构之间的翻译，并讨论迭代、尾递归与全递归函数。
扩展 PCF：Unit、Sum 与递归类型
为模型语言加入新的类型构造，理解它们的引入、消去与表达能力。
简单类型 Lambda 演算
系统整理类型、项、上下文相关语法，以及乘积类型与和类型。
等式、理论与证明系统
理解可推导关系的准确含义，以及语法证明如何组织成一套理论。
从通用代数理解代数数据类型
借助代数、签名、项和方程，把数据构造与代数规范联系起来。
命令式程序及其操作语义
进入位置、存储与 While 程序，形式化描述表达式求值和命令执行。
怎样选择阅读路线？
先读 00 建立全景，再按 01 → 10 前进，不必急着一次记住全部符号。
优先阅读 01—04 和 10，先掌握语法、语义、状态与程序执行。
完成 01—03 后跳到 06—09，集中理解类型构造、推导与代数结构。
学习程序语言理论的收获，并不只是在纸上描述一门小语言。它会逐渐改变你阅读真实程序的方式：哪些是语法限制，哪些是类型保证，哪些行为来自运行规则，也会因此分得更清楚。