使用Coq能否编写C程序？

Question

使用Coq能否编写C程序？

coqcoq-extraction

9

我知道可以将Coq程序提取成Haskell和OCaml程序。是否有办法用C语言做到这一点？

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

我会使用这样的库来构建一个对浮点数组进行快速排序的C算法，并能被GCC编译。

- Mark

2个回答

4

有一个新的软件基础章节，讨论了使用Coq和C进行接口设计的实践问题。

- Mark

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Arthur Azevedo De Amorim · Accepted Answer

Coq程序的提取目标不支持C语言，只支持OCaml和Haskell。然而，我们仍然可以使用Coq编写验证过的C语言软件：例如，Verified Software Toolchain允许我们将C程序翻译成Coq可以理解的格式并证明其行为的定理。请注意，如果您对Coq程序有任何证明经验，那么这些证明的风格会有所不同，因为C程序仅被转换为其语法树作为Coq数据类型，而不是Coq函数。