通过外部形式证明安全

Question

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

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

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

我知道证据承载代码，但它通常实现为一个传统的类型系统和编译器，证明在程序转换下的类型安全性。

Answer 1

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

当然，如果有两个这样的功能，可以选择一个优选的代码来生成代码。这也可以看作是产生可证实相同结果的优化。