外部正式証明による安全性

Question

安全性は一般的に強力な静的タイピングによって実装されます。非常に強力な型システム（依存型の型付け）がありますが、どれもコードに関する任意の正式な証明を表現するのに十分強力ではありません。別の問題は、タイプシステムが単一のプログラミング言語と緊密に結合され、正式なプルーフリファクタリングを禁止することである。

可能なフレームワーク私は、プログラマ（または自動化されたツール）がそれらを可能にする正式な証明を提供するとき、最適化を有効にするコンパイラを考えています。例としては、一意性、終了、配列境界チェック、メモリ管理、安全性などがあります。

何らかの方法でこの概念を実装しているプログラミング言語はありますか？

私は校正コードを知っていますが、これは通常、プログラム変換のもとで型安全性を証明する従来型システムとコンパイラとして実装されています。

Answer 1

Isabelle/HOLプルーフアシスタントのコードジェネレータは、あなたが記述した原則に基づいています。宣言的な方法で与えられる抽象的な関係を指定することができます。つまり、任意の入力に対して有効であることを確認する有効なアルゴリズムはありません（ただし、特定の入力に対しては証明できる可能性があります）。次に、任意の値に対して関係が成立するかどうかを調べる関数を定義します。これには、関数が計算可能であることを保証するためのいくつかのステップが含まれます。それが終わることを示す。次に、関係と機能が実際にお互いの代わりに使用できることが証明されます。最後に、この証明で、元の述語のコードを（サポートされている関数言語の1つで）生成するために関数を使用できることをIsabelleに伝えることが可能になります。

もちろん、このような関数が2つある場合は、コード生成に適した関数を選択することができます。これは、明らかに同一の結果をもたらす最適化として見ることもできる。