Вопрос про Agda:

[kouzdra]

А никто не знает - на ней хоть какие-то более или менее реальные программы писали, не обязательно сложные - на крайний случай и Тетрис какой-нибудь сойдет, но именно реальные.

PS: И тот же вопрос про Idris, хотя тут менее интересно.

Comments

[66george]

На их форуме посмотрите
https://lists.chalmers.se/mailman/listinfo/agda

[fuckind3r]

Это язык для доказательства теорем. Тетрис на нем писать глупо. Реальные теоремы о реальном коде доказывали.