是否可以使用 Coq 编写 C 程序？
Is it possible to write C programs using Coq?
我知道可以将 Coq 程序提取到 Haskell 和 OCaml 程序中。有没有办法用 C 做到这一点？
我正在想象一个模拟 C 语言的库。也许这样的库会包含一组关于 C 构造如何与进程内存交互的公理，以及关于 IEEE 浮点数的公理和定理。然后它将能够在 Coq 中构建一个 C 程序以及关于该程序的定理。
我会使用这样的库，比如说，构建一个适用于 GCC 可编译的浮点数组的 C 快速排序算法。
C 不可用作 Coq 程序的提取目标；仅支持 OCaml 和 Haskell。然而，我们仍然可以使用 Coq 来编写经过验证的 C 软件：例如，Verified Software Toolchain 允许我们将 C 程序转换为 Coq 理解的格式，并证明关于它们行为的定理。请注意，如果您对 Coq 程序做过任何证明，那么这些证明与您可能习惯的风格不同，因为 C 程序只是将其语法树转换为 Coq 数据类型，而不是 Coq 函数。
有一个新的 Software Foundations chapter 处理连接 Coq 和 C 的实践。
我知道可以将 Coq 程序提取到 Haskell 和 OCaml 程序中。有没有办法用 C 做到这一点？
我正在想象一个模拟 C 语言的库。也许这样的库会包含一组关于 C 构造如何与进程内存交互的公理，以及关于 IEEE 浮点数的公理和定理。然后它将能够在 Coq 中构建一个 C 程序以及关于该程序的定理。
我会使用这样的库，比如说，构建一个适用于 GCC 可编译的浮点数组的 C 快速排序算法。
C 不可用作 Coq 程序的提取目标；仅支持 OCaml 和 Haskell。然而，我们仍然可以使用 Coq 来编写经过验证的 C 软件：例如，Verified Software Toolchain 允许我们将 C 程序转换为 Coq 理解的格式，并证明关于它们行为的定理。请注意，如果您对 Coq 程序做过任何证明，那么这些证明与您可能习惯的风格不同，因为 C 程序只是将其语法树转换为 Coq 数据类型，而不是 Coq 函数。
有一个新的 Software Foundations chapter 处理连接 Coq 和 C 的实践。