When using Agda proofs, how can you know whether to trust it? Also, do they conform to a specific, well-defined type theory?

  • 4
    $\begingroup$ I think this question is actually a valid one, or at the very least very close to one. Agda has many features, many of which don't play well together and some of which are even unsound on their own. The fact that the specification of core Agda is the subject of current research makes the question "which part(s) of Agda have fully worked out, consistent theories" a good one. Voting to reopen. $\endgroup$
    – Josh
    Commented Feb 17, 2022 at 19:44
  • 5
    $\begingroup$ Is there something particular about Agda, or can we expect the same sort of question for every other proof assistant? If the latter, it would make sense to have a wiki question "What is known about the trustworthiness of major proof assistants?" or some such. $\endgroup$ Commented Feb 18, 2022 at 8:52
  • 5
    $\begingroup$ Are we supposed to "import" those questions? And why isn't Martín Escardó asking this? $\endgroup$ Commented Feb 18, 2022 at 18:25
  • 7
    $\begingroup$ So I can edit the question and turn it from a stub to a real one? $\endgroup$ Commented Feb 19, 2022 at 7:01
  • 3
    $\begingroup$ @AndrejBauer I would be glad if you did; I was thinking of doing so myself but your edit would probably be better $\endgroup$
    – Josh
    Commented Feb 19, 2022 at 12:23


Your Answer

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

Browse other questions tagged or ask your own question.