Лор, расскажи мне, как там дела с автоматическими пруф чекерами и соответственно с языками для написания дедуктивных доказательств? Появились ли уже вменяемые инструменты, которыми реально можно пользоваться, чтобы избавиться от ошибок в рассуждениях?
Знаю, что есть Петух (Coq), Агда и еще пара язычков, и что есть какая-то книжка Homotopy Type Theory, в которой все доказательства написаны на Петухе, но реально ли его использовать обычному человеку?
