Статья 320

Так получается язык динамических логик, которые зачастую имеют полную формализацию.
Множество возникающих принципиальных и технических трудностей привело к тому, что задача верификации программ - автоматизированного доказательства их правильности - остается до сих пор нерешенной.

Логическое описание программирования.

Мы видели, что уже для описания программы оказалось целесообразно воспользоваться аппаратом неклассической логики. Тем более это верно для задачи описания процесса программирования, когда самой программы еще нет и ее необходимо найти.
Для логиков было достаточно очевидно, что классическая логика плохо подходит для описания процесса программирования, поскольку она плохо подходит для описания процесса в математике. Еще в начале века было замечено, что в математике давно разошлись понятия существовать и быть построенным, трактовавшиеся с античных времен как синонимы.