24.07.2026
Пятничный язык программирования
Agda - это функциональный язык программирования с зависимыми типами, основанный на интуиционистской теории типов Пер Мартин-Лёфа и разрабатываемый группой Logic and Types в Чалмерском технологическом университете.
Язык поддерживает индуктивные семейства, параметризованные модули, mixfix-операторы, Unicode-символы и интерактивный Emacs-интерфейс. А еще язык используется для доказательства корректности программ
