c - 标准 ML 健全性证明？

Question

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

谢谢

Answer 1

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

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

这不是你的问题。

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