История изменений
Исправление quasimoto, (текущая версия) :
Таки да, зачем нужна агда человеку не занимающемуся профессионально математикой (ну или определённой математикой) или не участвующему в верификации с её помощью чего-либо, что требует верификации? Только теоремки for fun доказывать, разве что. Или вдохновиться и дальше писать на C++. Ещё в долгосрочной перспективе нельзя сказать наперёд — какое место займут зависимые типы и всё остальное что в языках типа агды происходит (а там много разного).
Исходная версия quasimoto, :
Таки да, зачем нужна агда человеку не занимающемуся профессионально математикой (ну или определённой математикой) или не участвующему в верификации с её помощью чего-либо, что требует верификации? Только теоремки for fun доказывать, разве что. Или вдохновиться и дальше писать на C++. Ещё в долгосрочной перспективе нельзя сказать наперёд — какое место займут зависимые типы и всё остальное что в языках типа агды происходит (а там много разного).