Jeśli Idris myśli, że rzeczy mogą być całkowite, które nie są, czy Idrys może być użyty do dowodów?

Question

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues stwierdza, że:

drugie, obecna implementacja miał ograniczony wysiłek włożony w to tak daleko, więc nie może być nadal przypadki, gdzie uważa funkcją jest całkowite, które nie jest. Nie licz na to jeszcze swoich dowodów!

Czy to oznacza, że ​​Idris nie może polegać na dowodach, czy też istnieje sposób na stworzenie dowodów, które nie wymagają sprawdzenia kompletności?

Answer 1

Wszyscy asystenci przeprowadzający testy narażają się na błędy związane z implementacją (a nawet błędy sprzętowe!), Które mogą spowodować niespójność systemu i umożliwić użytkownikom udowodnienie czegokolwiek. Ryzyko to nigdy nie może być zerowe. Nawet jeśli udowodnimy prawidłowość wdrożenia asystenta dowodowego, dowód ten należy udowodnić również w innym systemie formalnym lub nieformalnym, podlegającym temu samemu ryzyku.

Dlatego to, czego powinniśmy oczekiwać od asystenta dowodowego, nie jest nieomylną prawdą, jedynie mocnym dowodem słuszności. Jak silne są te dowody, zależy od naszych wcześniejszych informacji na temat wiarygodności systemu i stopnia, w jakim jesteśmy w stanie spojrzeć na konkretny dowód i ustalić, czy wykorzystuje niespójności.

A więc nie jest to jednoznaczny przypadek, jak mocne dowody stanowią dowody Idris. Powiedziałbym, że są dość silne w porównaniu z nieoficjalnymi dowodami. Również dowody Idrisona nie są jeszcze skalowalne aż do Agdy lub w szczególności dowodów Coqa, więc możliwe jest ich sprawdzenie przez ludzką inspekcję pod kątem "exploitów".