Вопрос про Agda:

[kouzdra]

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

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