Towards a Theory of Bugs: The Ruliology of the Unexpected
13 hours ago
- 程序中的意外行为通常源于计算不可约性，即不运行程序就无法预测其行为。
- 即使是图灵机和元胞自动机等简单系统也可能出现错误，这表明错误是计算中的基本现象。
- 由于计算不可约性，穷举测试程序是不可能的；错误可能罕见且难以检测，只有在处理大量案例后才会显现。
- 形式化证明可以验证某些程序的正确性，但可能需要任意长度的证明，并受限于计算不可约性。
- 语言设计（如 Wolfram 语言）通过提供与人类意图和计算可约性一致的原语，有助于减少错误。
- 规则学（对简单程序的研究）揭示，意外和错误普遍存在，挑战科学归纳法和预期。