Прежде чем мы расстанемся, я хотел бы предложить вам подумать о следующем способе отдать должное радикальной новизне вычислений в вводном курсе программирования.
С одной стороны, мы учим тому, что похоже на исчисление предикатов, но делаем это совсем не так, как философы. Чтобы обучить начинающего программиста манипулированию неинтерпретируемыми формулами, мы учим его больше как булевой алгебре, знакомя студента со всеми алгебраическими свойствами логических связок. Для дальнейшего разрыва ссылок на интуицию мы переименовываем значения {true, false} логического домена в {black, white}.
С другой стороны, мы учим простой, чистый, императивный язык программирования с пропуском и множественным присваиванием в качестве базовых операторов, со структурой блоков для локальных переменных, точкой с запятой в качестве оператора для композиции операторов, хорошей альтернативной конструкцией , хорошее повторение и, если нужно, вызов процедуры. К этому мы добавляем минимум типов данных, скажем, логические, целые числа, символы и строки. Существенным является то, что для того, что мы вводим, соответствующая семантика определяется соответствующими правилами доказательства.
С самого начала и на протяжении всего курса мы подчеркиваем, что задача программиста состоит не только в том, чтобы записать программу, но и в том, что его основная задача состоит в том, чтобы дать формальное доказательство того, что программа, которую он предлагает, отвечает в равной степени формальному функционалу Спецификация. При разработке доказательств и программ рука об руку студент получает широкие возможности для совершенствования своей маневренности с помощью исчисления предикатов. Наконец, чтобы донести до нас мысль о том, что этот вводный курс по программированию является в первую очередь курсом по формальной математике, мы проследим за тем, чтобы данный язык программирования не был реализован в кампусе, чтобы студенты были защищены от соблазна протестировать свои программы. , На этом я заканчиваю набросок моего предложения по вводному курсу программирования для первокурсников.