За какво е предназначена всяка от тези програми и какво предлага една на другата? Освен това и двете системи последователни ли са и освен това базирани ли са на някаква основополагаща математическа теория?
Две неща ме интересуват:
Търсих и това, което прочетох, изглежда много поляризирано, бих искал да знам разликите им от възможно най-обективната (човешка) гледна точка.
Coq е проектиран с мисъл за доказване на теорема, докато Agda е проектиран с мисъл за програмиране с зависим тип.
Те са донякъде еквивалентни от теоретична страна (въпреки че имат разлики, Coq е малко по-консервативен в своите аксиоми и се придържа по-близо до математическата основа на CIC по подразбиране), но бих им се доверил почти еднакво в този момент. Например, и двете се оказаха непоследователни в третирането си на коиндукция, но са доста устойчиви на грешки в обикновената индуктивна част.
Според моя опит и двете са лесни за инсталиране на Linux система. Agda може да е малко по-лесна, когато Cabal работи, но по-ужасна, когато не работи. Coq може да дойде в комплект или можете да го изградите от източника, според моя опит е добре, но понякога става болезнено, защото трябва да се грижите за версиите както на OCaml, така и на camlp5.
По отношение на ученето, мисля, че Coq може да бъде по-лесен за научаване, защото има някои съществуващи книги, които са доста дълги и бавни (Software Foundations, Coq'Art и т.н.) и някои книги за напреднали (CPDT). За Agda беше малко по-суров според моя опит, основно PDF на Norell и уикито... От друга страна, Agda изисква по-малко учене, защото най-вече трябва да grok зависими типове, синтаксис и стандартна библиотека. Докато в Coq трябва да научите и за тактиката, което е съвсем друго!
Моята гледна точка би била: - ако възнамерявате да правите голяма разработка с големи доказателства, Coq вероятно е вашият безопасен избор - ако просто се интересувате от програмиране с някои зависими типове, Agda вероятно е по-харесваният избор
Научаването на единия така или иначе ще помогне много за научаването на другия, така че защо не опитате по малко и от двете? :)
