Вопрос про Agda:

[kouzdra]

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

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

Comments

[thedeemon]

В одном из продуктов моей компании тыща строк на Идрисе использовалась (для генерации C#). Но там завтипы не очень активно использовались, с тем же успехом можно было на хаскеле или окамле написать.

[nivanych]

А почему про идрис менее интересно?
Из-за его строгости по умолчанию? ;-)

[kouzdra]

Скорее из-за его нетотальности по умолчанию.

[triampurum]

Про агду нет, а про Coq с экстракцией встречались саксесс стори. У nivanych и gds было что рассказать, кстати.

[kouzdra]

Coq-то вполне прикладная как раз система. На нем много чего пишут. Мне именно про Агду интересно - причем в основном не сакссес стори, а посмотреть как выглядят не примеры из статей про типы, а именно что-то реальное

[triampurum]

Гугль предлагает такое https://github.com/crypto-agda/protocols (и рядом там же). Для идриса такого, конечно, побольше.

grep на Agda

[dima_starosud]

github gallais aGdaREP

[nponeccop]

ACL2 возьмите и переводите в type theory :)