我看到几个不同的研究小组，以及至少一本书，都在谈论使用 Coq 来设计认证程序。对于认证项目的定义是否有共识？据我所知，它真正的意思是程序被证明是完全的并且类型正确。现在，程序的类型可能是非常奇特的东西，例如证明它是非空的、已排序的、所有元素 >= 5 等的列表。但是，最终，它是一个经过认证的程序，只有 Coq 显示的是完全的和类型安全的，所有有趣的问题都归结为最终类型中包含的内容？
编辑 1
根据 wjedynak 的回答，我查看了 Xavier Leroy 的论文“Formal Verification of a Realistic Compiler”，该论文链接在下面的答案中。我认为这包含了一些很好的信息，但我认为在这个研究序列中更多的信息可以在论文 Mechanized Semantics for the Clight Subset of the C Language 中找到。桑德琳·布拉齐和泽维尔·勒罗伊。这是“形式验证”论文添加优化的语言。在其中，Blazy 和 Leroy 介绍了 Clight 语言的语法和语义，然后在第 5 节讨论这些语义的验证。在第 5 节中，列出了用于验证编译器的不同策略，在某种意义上提供了一个概述创建认证程序的不同策略。这些都是:
无论如何，可能有几点可以补充，我当然想了解更多。
回到我最初的问题，即认证程序的定义是什么，我仍然有点不清楚。 Wjedynak 提供了一个答案，但实际上 Leroy 的工作涉及在 Coq 中创建一个编译器，然后在某种意义上对其进行验证。理论上，现在证明关于 C 程序的事情成为可能，因为我们现在可以进行 C->Coq->proof。从这个意义上说，似乎有这个工作流程我们可以
或者，我们可以在证明助手工具中创建程序的规范，然后证明关于该规范的属性，而不是程序本身。
无论如何，如果有人有替代定义，我仍然有兴趣听到它们。
最佳答案
我同意这个概念似乎含糊不清，但在我的理解中，经过认证的程序是配备/连同正确性证明的程序。现在，通过使用丰富且富有表现力的类型签名，您可以做到这一点，因此不需要单独的证明，但这通常只是为了方便。真正的问题是我们所说的正确性是什么意思:这是一个规范问题。你可以看看例如泽维尔·勒罗伊。 Formal verification of a realistic compiler .
关于coq - 认证程序的定义，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/21320138/