Coq和Agda之間的區別

Question

這些程序的每一個都是爲什麼而設計的？此外，這兩個系統是否一致，而且它們是基於一些基礎數學理論？

兩件事情我在乎：

1. 易於安裝
2. 易學

我搜索和我讀過似乎很極端，我想知道它們與最客觀（人性化）可能的觀點不同。

Answer 1

Coq的設計理念證明了這一點，而Agda設計時考慮了依賴型編程。

它們在理論上有些相同（儘管它們有區別，Coq在其公理中稍微保守一些，並且默認情況下更接近CIC的數學基礎），但是我相信它們在這一點上幾乎相等。例如，它們在共同誘導的處理上都被認爲是不一致的，但對於常規歸納部分中的錯誤非常有效。

根據我的經驗，它們都易於安裝在Linux系統上。當Cabal工作時，Agda可能會稍微容易一些，但如果沒有，則會更加糟糕。 Coq可以捆綁在一起，也可以從源代碼構建它，根據我的經驗它可以，但是有時會變得很痛苦，因爲你必須關心OCaml和camlp5的版本。在學習方面，我認爲Coq可能更容易學習，因爲它有一些現有的書籍相當長和節奏緩慢（軟件基礎，​​Coq'Art等）和一些高級書籍（CPDT）。對於Agda來說，根據我的經驗，它基本上是Norell的PDF和wiki ... 另一方面，Agda需要的學習較少，因爲您大多需要挖掘相關類型，語法和標準庫。而在Coq中，你也必須學習其他很多的策略！

我的觀點是： - 如果你打算做很大的樣張重大的研究與開發，勒柯克可能是你安全的選擇 - 如果你是在與一些相關類型的節目有興趣，阿格達可能是更可愛選擇

學習無論如何將有助於學習另一方面，所以爲什麼不嘗試一下呢？ :)