Здравствуйте, Эйнсток Файр, Вы писали:

ЭФ>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?

https://en.wikipedia.org/wiki/Self-verifying_theories
Хотя из их названия может показаться, что это какие-то "супер-теории", на самом деле они гораздо банальнее. Это такие искусствено урезанные, куцые теории (значительно слабее арифметики Пеано), в которых невозможно сформулировать диагональный аргумент. Чтобы доказать свою непротиворечивость, они просто говорят "мамой клянусь" — ну, то есть, у них просто есть аксиома о собственной непротиворечивости (впрочем, они действительно непротиворечивы, что можно доказать в арифметике Пеано). Они интересны просто как курьёзы, демонстрирующие технические требования для применимости теоремы Гёделя. Я очень сомневаюсь, что у них есть какая-либо связь с языками программирования, т.к. в них (насколько я понимаю) невозможно доказать даже базовые классические теоремы о вычислимых функциях.