When using Agda proofs, how can you know whether to trust it? Also, do they conform to a specific, well-defined type theory?
$\begingroup$
$\endgroup$
11
-
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$– JoshCommented 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$– Andrej BauerCommented 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$– Andrej BauerCommented 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$– Andrej BauerCommented 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$– JoshCommented Feb 19, 2022 at 12:23
|
Show 6 more comments