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

Question

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

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

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

Answer 1

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

Answer 2

有一个新的软件基础章节处理 Coq 和 C 接口的实践。