通过外部正式证明确保安全

Question

安全性通常通过强静态类型来实现。尽管有非常强大的类型系统（依赖类型），但它们都不足以表达关于代码的任意形式证明。另一个问题是类型系统与单一编程语言紧密耦合，抑制了形式证明的重构。

我正在考虑的一个可能的框架是一个编译器，当程序员（或自动化工具）提供允许优化的正式证明时，它会激活优化。例如唯一性、终止、数组边界检查、内存管理、安全等。

是否有任何编程语言以某种方式实现了这个概念？

我知道证明携带代码，但它通常被实现为常规类型系统和在程序转换下证明类型安全的编译器。

Answer 1

Isabelle/HOL 证明助手的代码生成器基于您描述的原理。可以指定以声明性方式给出的抽象关系，这意味着没有有效的算法来检查它是否适用于任意输入（尽管可能可以证明它适用于某些特定输入）。然后定义一个函数来检查关系是否适用于任意值。这包括一些确保函数可计算的步骤，例如表明它终止了。接下来，证明关系和函数确实可以相互替代使用。最后，有了这个证明，就可以告诉 Isabelle 该函数可用于为原始谓词生成代码（使用一种受支持的函数语言）。

当然，如果有两个这样的函数，可以选择一个首选的用于代码生成。这也可以被视为产生可证明的相同结果的优化。