Ну у меня на руках есть штука которая экстрактит из System Fw и библиотека под System Fw которая компилируется в байткод Erlang VM. Возможно надо с Черча на Паригота переписать, да и нафиг мне та индукция, писать же можно, термы конструировать. Теоремы писать какого-то уровня вы не сможете, но начального Хаскель или 1ML уровня код можно сделать быстрым и верифицируемым. Но только все это для платформы Эрланг.
Так что я бы не сказал, что это вообще нулевой результат.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2016-08-22 12:39 am (UTC)Так что я бы не сказал, что это вообще нулевой результат.