Статья 306

Если, например, переменная обозначается, то в терме величина обязана быть переменной для функции некоторый тип, и тогда весь этот терм имеет тип. Такая строгая дисциплина обеспечивает конечность вычислений термов с типами, если все входящие в них функции исчислимы за конечное время. В интерпретации Д. Скотта существенно то, что рассматриваются выражения без типов, а при конструировании программ естественнее как раз термы с типами.
В том же году Э. Бишоп подметил, что, если пользоваться не классической логикой и математикой, а конструктивной, то в принципе возможна цепочка чисто формальных преобразований.
Постановка задачи
Поиск вывода
Конструктивное доказательство
Извлечение программы
Программа
Наблюдение Бишопа стимулировало ряд работ по применениям конструктивной логики к программированию.
После того как активизировались работы по логическому описанию программ и программирования, стало видно, что логический анализ позволяет находить многие скрытые недоработки в концепциях языков программирования, анализировать эти концепции.