Coqを使用して認定プログラムを設計することについて話しているいくつかの異なる研究グループと、少なくとも1冊の本を見ています。認定プログラムの定義についてコンセンサスはありますか? 私が言えることは、それが本当に意味することは、プログラムが完全で型が正しいことが証明されたということだけです。現在、プログラムの型は、空でないこと、ソートされていること、すべての要素が 5 以上であることを証明するリストなど、非常にエキゾチックなものである可能性があります。ただし、最終的には、認定されたプログラムは、Coq が完全で型安全であることを示すものにすぎません。 、すべての興味深い質問は、最終的なタイプに何が含まれていたかに要約されますか?
編集 1
wjedynakの回答に基づいて、以下の回答にリンクされているXavier Leroyの論文「現実的なコンパイラの正式な検証」を見ました。これにはいくつかの良い情報が含まれていると思いますが、この一連の研究のより有益な情報は、Sandrine Blazy と Xavier Leroy によるC 言語の Clight サブセットのための機械化されたセマンティクスの論文で見つけることができると思います。これは、「Formal Verification」ペーパーが最適化を追加する言語です。その中で、Blazy と Leroy は Clight 言語の構文とセマンティクスを提示し、セクション 5 でこれらのセマンティクスの検証について説明します。セクション 5 には、コンパイラーの検証に使用されるさまざまな戦略のリストがあります。. これらは：
- マニュアルレビュー
- セマンティクスのプロパティの証明
- 検証済みの翻訳
- 実行可能なセマンティクスのテスト
- 代替セマンティクスとの同等性
いずれにせよ、おそらく追加できるポイントがあり、もっと詳しく聞きたいと思っています.
認定プログラムの定義は何かという最初の質問に戻りますが、それはまだ少し不明確です。Wjedynak は一種の答えを提供しますが、実際には Leroy の作業には、Coq でコンパイラを作成し、ある意味でそれを認定することが含まれていました。理論的には、C->Coq->証明に進むことができるようになったため、C プログラムに関することを証明できるようになりました。そういう意味では、こういうワークフローもありそうですね。
- X言語でプログラムを書く
- Coqまたはその他の証明補助ツールでのステップ1のプログラムのモデルの形式。これには、Coq でプログラミング言語のモデルを作成することが含まれる場合もあれば、プログラムのモデルを直接作成すること (つまり、Coq でプログラム自体を書き直すこと) が含まれる場合もあります。
- モデルに関するいくつかのプロパティを証明します。多分それは価値についての証明です。たぶん、それはステートメントの等価性の証明です（3 = 1 + 2またはf（x、y）= f（y、x）など）。
- 次に、これらの証明に基づいて、元のプログラムを認定済みと呼びます。
あるいは、プルーフ アシスタント ツールでプログラムの仕様を作成し、仕様に関するプロパティを証明できますが、プログラム自体は証明できません。
いずれにせよ、誰かが定義を持っているなら、私はまだ別の定義を聞くことに興味があります.