coq - 是否可以使用 Coq 编写 C 程序？

Question

我知道可以将 Coq 程序提取到 Haskell 和 OCaml 程序中。有没有办法用C来做到这一点？

我正在想象一个模拟 C 语言的库。也许这样的库将包含关于 C 构造如何与进程内存交互的公理集合，以及关于 IEEE 浮点数的公理和定理。然后它将能够在 Coq 中构建一个 C 程序以及关于该程序的定理。

例如，我会使用这样一个库来构建一个 C 快速排序算法，该算法适用于 GCC 可编译的浮点数组。

Answer 1

C 不能作为 Coq 程序的提取目标；仅支持 OCaml 和 Haskell。但是，我们仍然可以使用 Coq 编写经过验证的 C 软件:Verified Software Toolchain例如，允许我们将 C 程序转换为 Coq 理解并证明有关其行为的定理的格式。请注意，如果您对 Coq 程序进行过任何证明，这些证明的风格可能与您习惯的风格不同，因为 C 程序只是简单地转换为其语法树作为 Coq 数据类型，而不是 Coq 函数。