Mỗi chương trình trong số này được thiết kế cho những gì và mỗi chương trình nào khác cung cấp cho nhau? Ngoài ra, cả hai hệ thống đều nhất quán, và hơn thế nữa, chúng có dựa trên một số lý thuyết toán học cơ bản không?Sự khác biệt giữa Coq và Agda
Hai điều tôi quan tâm:
Tôi đã tìm kiếm và những gì tôi đã đọc dường như rất phân cực, tôi muốn biết sự khác biệt của họ từ quan điểm khách quan nhất (nhân văn).
Coq đã được thiết kế với định lý chứng minh trong tâm trí, trong khi Agda đã được thiết kế với lập trình phụ thuộc vào đánh máy.
Chúng có phần tương đương về mặt lý thuyết (mặc dù chúng có sự khác biệt, nhưng Coq khá thận trọng hơn trong các tiên đề của nó và gắn bó với nền tảng toán học của CIC theo mặc định), nhưng tôi sẽ tin tưởng chúng gần như bằng nhau tại điểm đó . Ví dụ, cả hai đã được tìm thấy là không phù hợp trong điều trị coinduction của họ, nhưng khá mạnh mẽ để lỗi trong phần quy nạp thường xuyên.
Theo kinh nghiệm của tôi, chúng đều dễ cài đặt trên hệ thống Linux. Agda có thể hơi dễ dàng hơn khi Cabal hoạt động, nhưng khủng khiếp hơn khi nó không hoạt động. Coq có thể đi kèm hoặc bạn có thể xây dựng nó từ nguồn, trong kinh nghiệm của tôi nó được ok, nhưng đôi khi nó được đau đớn bởi vì bạn phải quan tâm đến các phiên bản của cả hai OCaml và camlp5. Về mặt học tập, tôi nghĩ Coq có thể dễ học hơn vì nó có một số sách hiện có khá dài và chậm (Nền tảng phần mềm, Coq'Art, vv) và một số sách nâng cao (CPDT). Đối với Agda, nó hơi khó khăn hơn trong kinh nghiệm của tôi, về cơ bản là PDF và wiki của Norell ... Mặt khác, Agda đòi hỏi ít học tập hơn vì bạn chủ yếu phải gõ các kiểu phụ thuộc, cú pháp và thư viện chuẩn. Trong khi ở Coq bạn cũng phải tìm hiểu về chiến thuật mà là một toàn bộ rất nhiều khác!
Quan điểm của tôi sẽ là: - nếu bạn có ý định làm Phát triển lớn với bằng chứng lớn, Coq có lẽ là sự lựa chọn an toàn của bạn - nếu bạn chỉ quan tâm đến việc lập trình với một số loại phụ thuộc, Agda có lẽ là dễ thương hơn lựa chọn
Việc học tập sẽ giúp ích rất nhiều trong việc học cách khác, vậy tại sao bạn không thử một chút? :)
Mặt khác, thư viện chuẩn của Agda có thể được đọc để lvl trong FP với các kiểu phụ thuộc trong khi chúng là những phần rất lớn trong thư viện chuẩn của Coq quá cũ nên kiểu chứng minh không được chấp nhận. – gallais
Bạn đã xem http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq chưa? – user3237465
Chỉ cần làm, nhưng có rất nhiều điều mà tôi không hiểu vì điều này giả định bạn ít nhất là biết một trong số họ. –
Nếu có những điều bạn không hiểu ở đó, có lẽ họ thích hợp để hỏi ở đây? – didierc