Для чего предназначена каждая из этих программ и что они предлагают друг другу? Кроме того, согласованы ли обе системы и, более того, основаны ли они на какой-то фундаментальной математической теории?
Меня волнуют две вещи:
Я искал, и то, что я прочитал, кажется очень поляризованным, я хотел бы узнать их различия с наиболее объективной (с человеческой точки зрения) точки зрения.
Coq был разработан с расчетом на доказательство теорем, тогда как Agda был разработан с учетом программирования с зависимой типизацией.
Они в некоторой степени эквивалентны с теоретической точки зрения (хотя у них есть различия, Coq немного более консервативен в своих аксиомах и по умолчанию придерживается математической основы CIC), но в этом случае я бы им почти одинаково доверял. Например, было обнаружено, что они оба несовместимы в своем подходе к коиндукции, но довольно устойчивы к ошибкам в регулярной индуктивной части.
По моему опыту, их обоих легко установить в системе Linux. Agda может быть немного проще, когда Cabal работает, но еще ужаснее, когда это не так. Coq может поставляться в комплекте, или вы можете собрать его из исходников, по моему опыту, это было нормально, но иногда это становится болезненным, потому что вам нужно заботиться о версиях как OCaml, так и camlp5.
Что касается обучения, я думаю, что Coq может быть легче изучить, потому что у него есть некоторые существующие книги, которые довольно длинные и медленно развивающиеся (Software Foundations, Coq'Art и т. Д.), А также некоторые продвинутые книги (CPDT). По моему опыту, для Agda это было немного жестче, в основном PDF Norell и вики ... С другой стороны, Agda требует меньше обучения, потому что вам в основном приходится разбираться с зависимыми типами, синтаксисом и стандартной библиотекой. В то время как в Coq вы также должны изучить тактику, а это совсем другое дело!
Моя точка зрения была бы такой: - если вы намерены провести серьезную разработку с большими доказательствами, Coq, вероятно, ваш безопасный выбор - если вас просто интересует программирование с некоторыми зависимыми типами, Agda, вероятно, будет более подходящим выбором.
Изучение одного из них в любом случае очень поможет в изучении другого, так почему бы не попробовать и то, и другое? :)
