关于标准ML编译器，我的问题是，即使ML本身是正式定义的，也有可能证明对程序的确定性评估，不是用C编写的编译器本身(不是正式定义的)，至少不是全部吗？我想我的问题是说我们用Standard ML编写一个程序并可以证明其正确性，我们如何知道C编写的编译器没有以可能改变结果的方式执行？
谢谢
最佳答案
这是一个责任问题。无论您的SML运行时或编译器使用哪种语言编写(SML是一种规范，并且SML编译器而不是都必须站在C代码上，否则都可以)，您的责任是使SML程序根据SML规范。如果SML编译器有错误，那是别人的问题。
您是否考虑过要为处理器运行SML运行时的编译指令？谁正式证明了这一点？那么在处理器晶体管内部移动的电子又如何呢？谁告诉他们按照处理器设计所依据的物理“定律”进行工作？谁正式证明了这些法律？
这不是你的问题。
就是说，在撰写本文时，有一个基本上用Coq编写的C编译器CompCert。该编译器为输入语言(大部分C语言)和目标汇编语言定义了形式语义。只要将SML实现设计为在使用这种C语言进行编译时便可以正常使用C语言。如果您以CompCert的输入语言实现SML，请尽可能遵循正式的定义，充满信心的SML解释器几乎可以不中断地进行组装。
关于c - 标准ML健全性证明？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/20435282/