runtime-errors

如何证明你的代码没有运行时错误（以及为什么你很可能会放弃尝试）

抽象解释让你在执行之前就证明运行时错误不可能发生。以下是它的实际工作原理、难点所在，以及它在你的工具链中的定位。

你的测试套件通过了。你的类型检查器全是绿色。你发布了。两小时后，生产环境在一个没人想到要测试的边界情况上抛出了 。 测试能发现 bug。类型系统能预防一部分。但两者都无法证明你的程序完全没有运行时错误。要做到这一点，你需要更强力的手段：一种能够同时对所有可能的执行路径进行推理、而无需实际运行代码的方法。…