I've asked the same question on CSSE but with no luck (https://cs.stackexchange.com/questions/89611/is-agda-sound-as-a-proof-system). Therefore I ask it again here in cstheory and hope that more research-oriented audience can give more insights.

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's significantly much closer to Haskell than Coq.

However, I was quite a bit panicked when I see some code like following:

toList∘fromList : ∀ s → toList (fromList s) ≡ s
toList∘fromList s = trustMe

It seems there is an observable hole in the system, and it means Agda is not entirely built from ground up by axiomization. Then I saw this,


data Colist {a} (A : Set a) : Set a where
  []  : Colist A
  _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

I took Colist is the same as List in Haskell, allowing optionally infinite length, and from Wiki https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html

The type constructor ∞ can be used to prove absurdity!

Just as I suspected, optional infinity introduces absurdity. To this point, I felt I was more scared than amazed.

I understand that being practical must come with some trade off. However, Agda is more or less considered as a proof system, arguably more than a progarmming language. There are lots of papers these days are based on Agda. However, a quick code scan has shown holes in many disguises. (Sure Coq also has that, but it's considerably easy to discover: just grep axiom, admit will tell a lot, and Coq supports printing axioms for each lemma.)

Since I am trying to enter Agda, I have no idea what I should expect from it. So the title says all my question: are the system and the results based on it, sound?

  • 1
    $\begingroup$ Cross-posted: cstheory.stackexchange.com/q/40439/5038, cs.stackexchange.com/q/89611/755. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without anybody's time being wasted. $\endgroup$
    – D.W.
    Mar 23 '18 at 0:54
  • $\begingroup$ @D.W. if my question was read, nobody's time was wasted. i've explained why i posted here again. $\endgroup$
    – Jason Hu
    Mar 23 '18 at 0:56
  • 1
    $\begingroup$ I understand why it seems to make sense to you, but that's not how our site policies work. See the link I gave for explanation of why and details. (If you want the short version, just imagine what would happen if everyone did this -- but don't debate it here. See the link, and if you'd like to propose changing the policy, you can post on Theoretical Computer Science Meta. In the meantime, I hope you'll respect the site's policies.) $\endgroup$
    – D.W.
    Mar 23 '18 at 0:59