我知道可以将Coq程序提取到Haskell和OCaml程序中。有办法用C做到这一点吗？
我正在想象一个建模C语言的库。也许这样的库将包含有关C构造如何与进程内存交互的公理的集合，以及有关IEEE浮点数的公理和定理。这样一来，便可以在Coq中构建一个C程序以及有关该程序的定理。
我将使用这样的库来构建C快速排序算法，该算法可对GCC可以编译的浮点数组进行处理。
最佳答案
C不能用作Coq程序的提取目标；仅支持OCaml和Haskell。但是，我们仍然可以使用Coq来编写经过验证的C软件:例如，Verified Software Toolchain允许我们将C程序转换为Coq可以理解的格式并证明其行为的定理。请注意，这些证明与您完成有关Coq程序的证明时所用的风格有所不同，因为C程序只是作为Coq数据类型(而不是Coq函数)转换为语法树。
关于coq - 是否可以使用Coq编写C程序？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/46898518/