If Idris thinks things may be total that are not, can Idris be used for proofs?

Question

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues states that:

Secondly, the current implementation has had limited effort put into it so far, so there may still be cases where it believes a function is total which is not. Do not rely on it for your proofs yet!

Does this mean that Idris cannot be relied upon for proofs, or is there a way to create proofs that do not need the totality checker?

Criseyde

Answer 1

All proof assistants run the risk of implementation bugs (or even hardware bugs!) that may make the system inconsistent and allow users to prove anything. This risk can never be zero. Even if we prove the correctness of the implementation of a proof assistant, that proof also has to be proved in some other formal or informal system, subject to the same risks.

Therefore, what we should expect from a proof assistant is not infallible truth, merely strong evidence of validity. How strong that evidence is depends on our prior information about the trustworthiness of the system, and the extent to which we're able to look at a particular proof and determine whether it makes use of inconsistencies.

So, it's not a clear-cut case how strong evidence Idris proofs constitute. I would say they're quite strong in comparison to informal proofs. Also, Idris proofs don't yet scale as far as Agda or especially Coq proofs, so they are likely feasible to be checked by human inspection for "exploits".

Shiekh

Just merely strong evidence? I do not disagree with the fact of this answer but these tools are state of the art and the issues raised could not be overcome by any human endeavour. What a shame if someone read this and concluded there was no improvement over the fallibility of unit testing. – Babin