形式化并不是一个读完定义就算掌握的知识点，更像一组需要逐渐养成的阅读习惯：认出论文正在讨论的对象，跟上规则推动状态变化的过程，再判断分析结果究竟做出了怎样的保证。面对一整套新概念时，真正困难的往往不是某一页，而是不知道应该先读什么、后读什么。
这张阅读地图因此不急着讲具体公式，而是帮你安排路线。前六篇构成一条从“读懂符号”到“判断分析方法”的主线：前半程建立程序状态、语义与抽象的直觉，后半程把这些概念连成可运行的分析过程，并讨论可靠性、工程取舍以及人工智能生成代码带来的新问题。第七篇则离开技术主线，沿历史回看这些思想为何出现。
你可以从头走完全程，也可以根据手边的论文选择一段先读。下面每张卡片都说明了该篇要解决的问题，三种推荐路线则分别适合系统学习、临时补课和历史阅读。
不必把七篇文章当成必须一次完成的课程。 先解决眼前真正妨碍阅读的问题，再回来补齐前后联系，往往更容易形成自己的理解。
七篇文章
别怕公式：从集合、映射读懂程序状态
从最常见的符号开始，学会把形式化定义重新读成程序概念。
程序会走到哪里？从代码、CFG 到程序语义
换到分析器的视角，看见程序可能经过的路径以及状态如何变化。
不用记住每个值：从具体状态走向抽象解释
理解分析器为什么必须忘掉一些细节，又如何保留真正重要的性质。
分析器为什么会停下来？从传递函数到不动点
跟着信息在程序中传播，理解循环分析最终怎样得到稳定结果。
准确、快速，还是可靠？静态分析的工程取舍
把公式放回现实工具，判断一项分析究竟承诺了什么、牺牲了什么。
AI 写完代码，谁来验收？
当大模型开始生成程序，重新追问“看起来正确”和“可以相信”之间的距离。
历史篇：从“什么是计算”到“如何相信程序”
沿着历史回望，这些今天熟悉的形式化思想为何会被一步步发明出来。
怎样选择阅读路线？
按照 01 → 06 阅读，最后用历史篇换一个视角回看整条路线。
先读 01 和 02 建立读法，再根据论文内容跳到对应篇章。
可以直接阅读 07。它不要求提前读完前六篇，也不会重复主线内容。
形式化并不会因为读完一个系列就突然变得简单，但它会开始变得可以拆解。下一次在论文中遇到陌生公式时，你不必再整段跳过，而会知道先去哪里找对象、关系和规则——这正是这七篇文章想交给你的阅读能力。