2
$\begingroup$

If I understand it, this video series mentioned that idris2 currently has some type-in-type problems, so that one can exploit it to prove false claims. I am not familiar with the concept, and am concerned whether I should learn idris2 as a proof assistant/language. The speaker said then that it will probably be fixed sometime in the future, but it is not clear whether that has happened (as of 0.6.0).

So my questions are:

What's a good example of the type-in-type problem that leads to a falsely proved claim?

If one uses idris2 as a proof language, is there a way to use it carefully (in a disciplined way) to avoid the "type-in-type" problem?

$\endgroup$

1 Answer 1

2
$\begingroup$

See the following references:

In principle you cannot know for sure whether type-in-type creeped in somehow and caused a problem, and it has been known to happen, as discussed in Has anyone ever accidentally "proven" a false theorem with type-in-type?. However, I would say you should just go ahead and use Idris. So long as you're doing "normal" things, it should be ok. Also, it's exciting to live dangerously.

$\endgroup$
1
  • 1
    $\begingroup$ For concreteness, an example usage of the Hurkens package in Coq is: From Coq Require Import Hurkens. Unset Universe Checking. Definition Hurkens'_paradox := PropNeqType.paradox eq_refl : False. $\endgroup$
    – djao
    Aug 26, 2023 at 9:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.