是否可以使用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函数转换为其语法树.