Idrisが物事が完全ではないと思ったら、Idrisは証明のために使用できますか？

Question

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issuesと述べている：

は、第二に、現在の実装では、これまでのところ、それに入れ限られた努力があったので、まだそれは機能がされていない合計であると考えている場合もあります。まだあなたの証明のためにそれに頼らないでください！

これは、Idrisが証明のために信頼できないことを意味しますか、または完全性チェッカーを必要としない証明を作成する方法はありますか？

Answer 1

すべてのプルーフアシスタントは、システムに一貫性がなくユーザーが何かを証明できるようにする実装上のバグ（またはハードウェアのバグ）の危険性があります。このリスクはゼロになることはありません。証拠補助の実施の正当性を証明したとしても、その証拠は、他の公式または非公式のシステムで証明されなければならず、同じリスクがあります。

したがって、証明アシスタントから期待するべきことは、間違いない真実ではなく、単に妥当性の強い証拠です。その証拠がどれほど強いかは、システムの信頼性に関する以前の情報、および特定の証明を見て、それが矛盾を利用するかどうかを判断できる程度に依存します。

したがって、Idrisの証明がどれほど強力な証拠であるかは、明確なケースではありません。私は彼らが非公式の証拠と比べてかなり強いと言います。また、Ididの証明は、Agdaや特にCoqの証明まではスケールされていないので、人間の検査で「悪用」をチェックすることは可能です。