标准ML健全性证明？

Question

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

谢谢

Answer 1

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

\n\n

您是否考虑过为 SML 运行时运行的已编译指令所运行的处理器？谁正式证明了这一点？那么在处理器晶体管内移动的电子又如何呢？谁告诉它们按照处理器设计所依据的物理原理 \xe2\x80\x9claws\xe2\x80\x9d 工作？谁正式证明了这些定律？

\n\n

这不是你的问题。

\n\n

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

\n