Статья 350

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