http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues 상태는 것을 :이드리스가 일이 합계가 아니라고 생각한다면, 이드리스를 교정 용으로 사용할 수 있습니까?
둘째, 현재 구현했다 제한 노력은 지금까지 들어가 있기 때문에, 아직이 기능을하지 않은 총 믿는 경우가있을 수 있습니다. 아직 그 증거에 의존하지 마십시오!
Idris가 교정본에 의존 할 수 없거나 전체 검사기가 필요하지 않은 교정본을 만드는 방법이 있습니까?
모든 증명 보조원은 시스템을 일관성 없게 만들고 사용자가 무엇이든 증명할 수 있도록 구현 버그 (또는 하드웨어 버그!)의 위험을 감수합니다. 이 위험은 결코 0이 될 수 없습니다. 우리가 증명 조력자의 수행의 정확성을 증명한다고해도, 그 증명은 다른 형식적 또는 비공식적 인 시스템에서도 입증되어야하며, 동일한 위험을 감수해야합니다.
따라서 증명 보조자가 기대해야 할 것은 절대적인 진실이 아니라 단지 타당성에 대한 강력한 증거입니다. 그 증거가 얼마나 강한지는 시스템의 신뢰성에 대한 사전 정보와 특정 증거를보고 불일치를 사용하는지 여부를 판단 할 수있는 정도에 달려 있습니다.
따라서 이드리스 교정이 얼마나 강력한 증거인지는 분명하지 않습니다. 나는 그들이 비공식적 인 증거에 비해 꽤 강하다고 말한다. 또한 이드리스 교정은 Agda 또는 특히 Coq 교정본까지는 확장 할 수 없으므로 인위적인 검사로 "악용 사례"를 확인하는 것이 타당합니다.
그냥 * 단지 * 강한 증거? 이 답변의 사실에 동의하지는 않지만 이러한 도구는 예술 수준이며 제기 된 문제는 인간의 노력으로 극복 할 수 없습니다. 누군가이 사실을 읽고 단서 테스트의 오류 가능성에 대한 개선이 없다고 결론을 내리면 참으로 안타깝습니다. – erisco