Coqを使ってCプログラムを書くことは可能ですか？

Question

私は、HaskellとOCamlプログラムにCoqプログラムを抽出できることを知っています。 Cでこれを行う方法はありますか？

私はC言語をモデル化したライブラリを想像しています。おそらく、そのようなライブラリには、C構造がプロセスメモリとどのようにやりとりするか、そしてIEEE浮動小数点数に関する公理と定理についての公理の集合が含まれるでしょう。それから、プログラムについての定理とともにCoq内にCプログラムを構築することができます。

GCCでコンパイル可能な浮動小数点数の配列に作用するCクイックソートアルゴリズムを構築するために、このようなライブラリを使用します。

Answer 1

CはCoqプログラムの抽出対象にはなりません。 OCamlとHaskellだけがサポートされています。しかし、検証済みのCソフトウェアを書き込むためにCoqを使用することができます。たとえば、Verified Software Toolchainは、CプログラムをCoqが理解し、その動作についての定理を証明する形式に翻訳することを可能にします。これらの証明は、CプログラムがCoq関数ではなくCoqデータ型として構文ツリーに単純に変換されるため、Coqプログラムについて何らかの証明を行った場合とは異なる風味があることに注意してください。