Без заголовка

HOL здесь не спасёт, с ней будут те же самые ляпы. Код предметной области можно проверить и отладить на самой предметной области. А для логического описания мы можем выяснить непротиворечивость, но крайне сложно проверить его адекватность описываемой ситуации. Короче говоря, если факты сами себя обрабатывают, то это плохая обработка, а также препятствие для удобной обработки этих фактов чем-либо ещё. Мне кажется, что единственным решением является отсутствие навороченных механизмов вывода в языке. Вывод (даже прототипный) надо оставить имплементациям, и он может влиять на "циферки", но не должен влиять на базовую систему типов.