通過外部形式證明安全

Question

安全通常通過強大的靜態打字來實現。雖然有非常強大的類型系統（依賴打字），但它們都不足以表達對代碼的任意形式證明。另一個問題是類型系統與單一編程語言緊密耦合，抑制了形式化證明重構。

我在想的一個可能的框架是編程器，它在程序員（或自動化工具）提供正式證明時允許它們激活優化。例子是唯一性，終止，數組邊界檢查，內存管理，安全等。

是否有任何編程語言實現某種方式這個概念？

我知道證據承載代碼，但它通常實現爲一個傳統的類型系統和編譯器，證明在程序轉換下的類型安全性。

Answer 1

Isabelle/HOL證明助理的代碼生成器基於您描述的原則。可以指定以聲明方式給出的抽象關係，這意味着沒有有效的算法來檢查它是否適用於任意輸入（儘管可能可以證明它用於某些特定輸入）。然後，定義一個函數來檢查關係是否適用於任意值。這包括確保該功能是可計算的一些步驟，例如，以表明它終止。接下來，我們證明關係和函數確實可以用來代替對方。最後，通過這個證明，有可能告訴Isabelle該函數可用於爲原始謂詞生成代碼（使用支持的函數語言之一）。

當然，如果有兩個這樣的功能，可以選擇一個優選的代碼來生成代碼。這也可以看作是產生可證實相同結果的優化。