автоматический доказатель

После нового года опять заработал мехматовский семинарчик по логике. Сейчас Женя Беркович на доске программирует в примитивно-рекурсивных функциях лямбда-исчисление. Доказывает, что они эквивалентны. Можно подумать кто-то сомневался. Но есть же любители.

В перерывах между смотрением на доску, скачал книгу Logic in Computer Science 2nd - Huth & Ryan.PDF. Я под впечатлением от открытия для себя изоморфизма Кари-Говарда, автоматического доказателя теорем Coq, а так же созданного с его помощью формально доказанного компилятора Compsert. Жду не дождусь, когда компьютеры заменят программистов.