Статья 305

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