信任

Lean 的核心价值之一在于它能够构建数学证明，包括关于程序正确性的证明。用户经常提出的一个问题是：我们能够多大程度地信任 Lean，以及具体需要信任哪些部分。

这个问题的答案包含两个方面：用户需要信任哪些部分才能相信 Lean 中的证明，以及用户需要信任哪些部分才能相信通过编译 Lean 程序获得的可执行程序。

具体来说，区别在于：证明（包括关于程序的陈述）和未编译的程序可以直接用 Lean 的内核语言表达，并由内核对实现进行检查。它们不需要被编译成可执行文件，因此信任仅限于检查它们的内核实现，暂时不用信任 Lean 编译器。

信任已编译 Lean 程序的正确性需要信任 Lean 的编译器，而编译器与内核是分离的，不属于 Lean 的核心逻辑。信任 Lean 中 关于程序的陈述 与信任 Lean 编译器生成的程序 是两回事。关于 Lean 程序的陈述是证明，属于仅需信任内核的范畴。而信任关于程序的证明 能推广到已编译程序的行为 则会将编译器纳入可信代码库。

注意：策略（tactics）和其他元程序（metaprograms），即使是已编译的策略，也 完全不需要 被信任；它们是非可信代码，仅用于生成供其他部分使用的内核项。命题 P 可以通过任意复杂的已编译元程序在 Lean 中证明，而无需将可信代码库扩展到内核之外，因为元程序必须生成用 Lean 内核语言表达的证明。

  • 这些陈述适用于导出的证明。为了让更 挑剔 谨慎的读者满意，这确实需要在某种程度上信任其他部分，例如运行导出器和验证器的计算机操作系统、硬件等。

  • 对于未导出的证明，用户还需要额外信任内核之外的 Lean 组件（如繁饰器（elaborator）、解析器等）。

更详细的清单

关于 Lean 4 中信任问题的更详细说明来自 Mario Carneiro 在 Lean Zulip 上的帖子。

一般来说：

  1. 你需要信任Lean的逻辑是可靠的（作者注：这包括任何内核扩展，例如 Nat 和 String 的扩展）

  2. 如果你没有证明程序的正确性，你需要信任繁饰器已将你的输入转换为符合预期的 Lean 表达式

  3. 如果你确实证明了程序的正确性，你需要信任关于程序的证明已被检查（可通过外部检查器消除此需求）

  4. 你需要信任运行这些程序的硬件/固件/操作系统软件没有出错或欺骗你

  5. （运行程序时）你需要信任硬件/固件/操作系统软件能按照规范忠实地执行程序，并且没有调试器、硬盘上的磁铁或宇宙射线干扰输出

对于已编译的可执行文件：

  1. 你需要信任任何编译器覆盖（extern / implemented_by）没有违反 Lean 逻辑（即模型与实现匹配）

  2. 你需要信任Lean编译器（将 Lean 代码降级为 C 代码）能保持程序的语义

  3. 你需要信任 clang/LLVM 能将 C 程序转换为具有相同语义的可执行文件

第一组要点适用于证明和已编译的可执行文件，而第二组专门针对已编译的可执行程序。

对外部检查器的信任

  1. 你仍然需要信任Lean的逻辑是可靠的。

  2. 你需要信任外部检查器的开发者正确实现了该程序。

  3. 你需要信任实现语言的编译器或解释器。如果运行多个外部检查器，你可以将它们视为维恩图中的圆圈；你需要信任这些圆圈重叠的部分没有可靠性问题。

  4. 对于 Nat 和 String 的内核扩展，你可能需要信任一个大数库和实现语言的 UTF-8 字符串类型。

使用外部检查器的优势包括：

  • 用户可以用完全独立于 Lean 生态系统的工具检查结果，不依赖于 Lean 代码库的任何部分。

  • 外部检查器可以利用成熟的编译器或解释器实现。

  • 对于内核扩展，用户可以交叉检查多个大数/字符串实现的结果。

  • 使用导出功能是摆脱对 Lean 内核之外部分信任的唯一方法，因此即使导出文件是通过 lean4lean 等工具检查的，这样做也有好处。因此，担心滥用 Lean 元编程功能可能带来影响的用户被鼓励使用导出功能。