red*_*h64 7 proof idris totality
http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出:
其次,到目前为止,目前的实施工作进展有限,因此可能仍然存在一种情况,即它认为功能是总的而不是.不要依赖它来证明你的证明!
这是否意味着不能依赖Idris作为证据,或者是否有办法创建不需要整体检查的证明？
所有证明助手都面临着实施错误(甚至是硬件错误!)的风险,这些错误可能会使系统不一致并允许用户证明任何事情.这种风险永远不会为零.即使我们证明了证明助手实施的正确性,该证据也必须在其他正式或非正式系统中得到证明,并承担相同的风险.
因此,我们应该从证明助理那里得到的不是绝对正确的事实,而只是有效性的有力证据.证据的强大程度取决于我们关于系统可信度的先验信息,以及我们能够在多大程度上查看特定证据并确定其是否利用不一致性.
因此,Idris证据构成的强有力证据并不是一个明确的案例.我会说他们与非正式证据相比非常强大.此外,Idris样张尚未扩展到Agda或特别是Coq样张,所以它们可能可以通过人工检查来检查"漏洞".