Ну у меня на руках есть штука которая экстрактит из System Fw и библиотека под System Fw которая компилируется в байткод Erlang VM. Возможно надо с Черча на Паригота переписать, да и нафиг мне та индукция, писать же можно, термы конструировать. Теоремы писать какого-то уровня вы не сможете, но начального Хаскель или 1ML уровня код можно сделать быстрым и верифицируемым. Но только все это для платформы Эрланг.

Так что я бы не сказал, что это вообще нулевой результат.