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

<hr>

<p>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.</p>

<p>However, I was quite a bit panicked when I see some code like following:</p>

<pre><code>toList∘fromList : ∀ s → toList (fromList s) ≡ s
toList∘fromList s = trustMe
</code></pre>

<p>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,</p>

<p><a href="https://github.com/agda/agda-stdlib/blob/master/src/Data/Colist.agda" rel="noreferrer">https://github.com/agda/agda-stdlib/blob/master/src/Data/Colist.agda</a></p>

<pre><code>data Colist {a} (A : Set a) : Set a where
  []  : Colist A
  _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
</code></pre>

<p>I took <code>Colist</code> is the same as <code>List</code> in Haskell, allowing optionally infinite length, and from Wiki <a href="https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html" rel="noreferrer">https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html</a></p>

<blockquote>
  <p>The type constructor ∞ can be used to prove absurdity!</p>
</blockquote>

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

<p>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.)</p>

<p>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?</p>

CC BY-SA 3.0
2018-03-23T00:54:44.060Z
Cross-posted: https://cstheory.stackexchange.com/q/40439/5038, https://cs.stackexchange.com/q/89611/755.  Please [do not post the same question on multiple sites](https://meta.stackexchange.com/q/64068). Each community should have an honest shot at answering without anybody's time being wasted.
D.W.
CC BY-SA 3.0
2018-03-23T00:56:53.910Z
@D.W. if my question was read, nobody's time was wasted. i've explained why i posted here again.
Jason Hu
CC BY-SA 3.0
2018-03-23T00:59:59.600Z
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 [meta].  In the meantime, I hope you'll respect the site's policies.)
D.W.
<lo.logic><proof-assistants>
Is Agda sound as a proof system?
Jason Hu
# Is Agda sound as a proof system?

(Asked by: username_0 on 2018-03-22)

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,
https://github.com/agda/agda-stdlib/blob/master/src/Data/Colist.agda
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?

**Tags:** lo.logic, proof-assistants
> **Comments:**
> **username_1**: Cross-posted: https://cstheory.stackexchange.com/q/40439/5038, https://cs.stackexchange.com/q/89611/755.  Please [do not post the same question on multiple sites](https://meta.stackexchange.com/q/64068). Each community should have an honest shot at answering without anybody's time being wasted.  
> **username_0**: @D.W. if my question was read, nobody's time was wasted. i've explained why i posted here again.  
> **username_1**: 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 [meta].  In the meantime, I hope you'll respect the site's policies.)  

---

## 0 answers

