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?

  • $\begingroup$ really nobody wants to answer this question? $\endgroup$
    – Jason Hu
    Mar 22 '18 at 16:17
  • $\begingroup$ is it a good idea to ask this question on cstheory, in case there can be more attention on that platform. $\endgroup$
    – Jason Hu
    Mar 22 '18 at 16:29
  • 2
    $\begingroup$ I encourage you to have some more patience. This is a small site; sometimes it can take a few days for people to see the question. You could consider setting a bounty if you want to try to gather more attention to the question, but I'd recommend just giving it a little time. $\endgroup$
    – D.W.
    Mar 23 '18 at 0:55
  • 3
    $\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:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.