Статья 355

Дескриптивные описания недетерминированных операторов в несколько раз короче. А в конструктивном случае различие становится просто катастрофическим, и порою нет средств построить полную конструктивную систему для детерминированного случая.
Впервые на силу логики в качестве инструмента анализа понятий программирования обратили внимание в середине 70-х годов в связи с развитием теории верификации программ. Оказалось, что для многих конструкций совместное использование которых не приводит к алгоритмической невычислимости, невозможно построить полную формальную систему, описывающую их взаимодействие.
Например, только при многочисленных безуспешных попытках описания процедур с побочным эффектом и присваиваний над массивами стало ясно, насколько неприятные и замаскированные неожиданности подстерегают нас здесь.