http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出：
其次，目前的实现到目前为止所做的努力有限，因此可能仍然存在它认为一个函数是完全的但不是的情况。不要依赖它来做你的证明！
这是否意味着不能依赖 Idris 来提供证明，或者有没有一种方法可以创建不需要整体检查器的证明？
问问题
255 次
1 回答
9
所有的证明助手都有实现错误（甚至硬件错误！）的风险，这可能会使系统不一致并允许用户证明任何事情。这种风险永远不可能为零。即使我们证明了证明助手实现的正确性，该证明也必须在其他一些正式或非正式的系统中得到证明，面临同样的风险。
因此，我们应该从证明助理那里得到的不是绝对正确的真理，而仅仅是有效的有力证据。证据的强度取决于我们关于系统可信度的先前信息，以及我们能够查看特定证据并确定它是否利用不一致的程度。
因此，伊德里斯证明构成的有力证据并不是一个明确的案例。我会说它们与非正式证明相比非常强大。此外，Idris 证明还没有像 Agda 或特别是 Coq 证明那样扩展，因此它们很可能可以通过人工检查来检查“漏洞”。
于 2016-12-13T10:43:29.097 回答