标准 ML 健全性证明？答案

【问题标题】：Standard ML Proof of soundness?标准 ML 健全性证明？
【发布时间】：2013-12-06 23:15:02
【问题描述】：

关于标准 ML 编译器，我的问题是，尽管 ML 本身是正式定义的，可以证明程序的确定性评估，但编译器本身不是用 C 编写的，它没有正式定义，至少不是全部?我想我的问题是说我们用标准 ML 编写了一个程序并且可以证明它的正确性，我们怎么知道 C 编写的编译器没有以可能改变结果的方式执行？

谢谢

【问题讨论】：

请注意，大多数 ML 编译器不是用 C 编写的，除了运行时系统的一些小部分。他们中的大多数（全部？）实际上是在 ML 中引导的。不过，这是个好问题。
错误可以以任何语言出现在任何地方。如果正式验证器有错误怎么办？如果编译正式验证器的编译器将错误引入其中怎么办？最终很难从数学上确定复杂系统的行为。所有这些都是使用易受宇宙射线、制造缺陷和良好量子不确定性影响的电子设备实现的。
@Potatoswatter：“如果形式验证器有错误怎么办？”：这是一个很好的问题，蚂蚁要回答这个问题，有证明者依赖于小的可信内核（最小，更可信），比如LCF、Isabelle 和其他一些 LCF 变体。所有更高级别的证明显然必须通过这个小内核并且永远不会绕过它。
有一个正式验证的 SML 实现叫做 CakeML，查看cakeml.org

标签： c compiler-construction sml ml

【解决方案1】：

这是一个责任问题。无论您的 SML 运行时或编译器是用什么语言编写的（SML 是一种规范，而 SML 编译器不必必须基于 C 代码，它可以是其他任何语言），您的责任是让您的 SML根据 SML 规范进行程序工作。如果 SML 编译器有问题，那是别人的问题。

您是否考虑过运行 SML 运行时编译指令的处理器？谁正式证明了这一点？那么在处理器晶体管内部移动的电子呢？谁告诉他们按照处理器设计所依据的物理“定律”工作？谁正式证明了这些定律？

这不是你的问题。

也就是说，在撰写本文时，有一个 C 编译器，基本上是用 Coq 编写的，CompCert。该编译器为输入语言（大部分 C）和目标汇编语言定义了形式语义。输入语言不必完全是 C，只要 SML 实现设计为在使用这种风格的 C 编译时工作。如果您在 CompCert 的输入语言中实现 SML，尽可能遵循正式定义，您将有一个具有信心链的 SML 解释器几乎不间断地进行组装。

【讨论】：

我喜欢这个答案，它完全有道理，但我想我的问题是所有在 SML 下运行的定理证明软件，这不完全取决于 C 编译器的正确性吗？使用？所以确定用于证明某事的 SML 在理论上可能是合理的，但我们依靠 C 来成功编译，这无法证明是正确的。
@SJP 你会喜欢这篇博文，如果你还没有看过的话：blog.regehr.org/archives/903。但无论如何，我们不需要对我们的程序有绝对的信心，因为我们没有绝对有信心在其上执行它们的机器。在计算中只需要一个 alpha 粒子来改变一点。各种形式的方法都提供了信心的方式，远远超过了传统的技术。尝试使用它们的人看到的问题不是编译器错误导致验证系统不健全的可能性，而是成本，这是我们首先应该关注的问题

【解决方案2】：

仅仅因为您可以编写糟糕的 C 程序并不意味着您必须这样做。完全有可能编写一个正确的 C 程序并从 C 语言规范中推断该程序正确执行。

【讨论】：

另外，至少存在一种形式化证明的C编译器，即CompCert。