История изменений
Исправление Manhunt, (текущая версия) :
Эта задача, вообще говоря, неразрешима.
В общем случае доказательство лежит на плечах программиста. Чтобы такое программирование было хоть сколько-нибудь практичным, нужно:
1. напихать в компилятор эвристики и схемы доказательств для типовых случаев/ситуаций
2. реализовать язык подсказок, на котором программист будет указывать, какую именно из схем доказательств к каким именно точкам кода нужно приятнуть, чтобы солвер смог построить доказательство
Пока мы от этого удручающе далеки.
Исходная версия Manhunt, :
Эта задача, вообще говоря, неразрешима.
В общем случае доказательство лежит на плечах программиста. Чтобы такое программирование было хоть сколько-нибудь практичным, нужно:
1. напихать в компилятор эвристики и схемы доказательств для типовых случаев/ситуаций
2. реализовать язык подсказок, на котором программист будет указывать, какую именно из схем доказательств к каким именно точкам кода нужно приятнуть, чтобы солвер смог построить доказательство