一份写给研究生和软件分析爱好者的形式化阅读地图，帮助你跨过程序分析论文中定义与公式的门槛。

A reading guide for students who want to make sense of the definitions, notation, and rules in program analysis papers.

Follow a small search page from loading to interaction, and learn where web code runs, how events trigger execution, and how data crosses the browser/server boundary.

Codex 经常因网络问题连续重试？用一个启动脚本同时配置代理环境变量和桌面端代理参数。

从图灵追问什么是计算，到现代工具验证真实软件：沿着关键人物与思想，重走程序语言形式化近百年的历史。

Follow the people and problems behind computation, program semantics, verification, and modern formal methods.

大模型生成的代码看起来正确，就真的值得信任吗？从测试、验证与证明出发，重新理解 AI 编程时代的可靠性边界。

Connect AI-generated code to specifications, testing, verification, and the limits of formal guarantees.

静态分析不可能同时拥有绝对准确、极致速度和无限规模。读懂可靠性、精度与工程成本之间真正的取舍。

Understand what an analysis guarantees, why false positives arise, and how precision and cost shape real tools.