Idris 2 теперь стал self-hosted

Я спрошу здесь: а зачем они нужны эти Idris, Agda, Coq? Для доказательств теорем? Надо попробовать когда-то.

Например можно доказать коммутативность сложения на агде. Классно, но хз зачем я это сделал

Идрис - это general purpose, с практичными зависимыми типами.

Как я понимаю, Coq в первую очередь для доказательств теорем. Например, можно доказать что какой-то язык обладает определёнными свойствами. Или что нибудь более «чисто» математическое.

Идрис разрабатывается с прицелом на практическое применение. Т.е. это язык программирования в обычном понимании этого термина. Вроде Хаскеля, но с зависимыми типами. Т.е. доказывать теоремы в нём тоже можно, но может быть не так удобно. Но главное (должно быть) удобно программировать.

Агда, на сколько я знаю, была разработана как система доказательств теорем. Но если мне не изменяет память были попытки отдельных людей сделать упор на практике, путём написания библиотек. Однако, не знаю чем они закончились.

Спасибо за новость!