如果 Idris 认为事物可能是整体的，那么 Idris 可以用于证明吗？答案

【问题标题】：If Idris thinks things may be total that are not, can Idris be used for proofs?如果 Idris 认为事物可能是整体的，那么 Idris 可以用于证明吗？
【发布时间】：2016-12-13 03:48:07
【问题描述】：

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues 声明：

其次，目前的实现到目前为止所付出的努力有限，因此可能仍然存在它认为一个函数是完全的但不是的情况。暂时不要依赖它来证明！

这是否意味着不能依赖 Idris 来提供证明，或者有没有办法创建不需要整体检查器的证明？

【问题讨论】：

标签： proof idris totality

【解决方案1】：

所有证明助手都存在实施错误（甚至是硬件错误！）的风险，这可能会使系统不一致并允许用户证明任何事情。这种风险永远不可能为零。即使我们证明了证明助手实现的正确性，该证明也必须在其他一些正式或非正式的系统中得到证明，面临同样的风险。

因此，我们应该从证明助理那里得到的不是绝对正确的真理，而是有效的有力证据。证据的强度取决于我们关于系统可信度的先前信息，以及我们能够查看特定证据并确定它是否利用不一致的程度。

因此，Idris 的证明构成了多么有力的证据并不是一个明确的案例。我会说它们与非正式证明相比非常强大。此外，Idris 证明还没有像 Agda 或特别是 Coq 证明那样扩展，因此它们很可能可以通过人工检查来检查“漏洞”。

【讨论】：

只是只是有力的证据？我不同意这个答案的事实，但这些工具是最先进的，所提出的问题是任何人类努力都无法克服的。如果有人读了这篇文章并得出结论认为单元测试的易错性没有任何改善，那真是太可惜了。