Вместо обучения императивщине последовательностям выполнения инструкций, привязанных к синтаксису конкретного языка, что сильно сбивает начинающих, которые начинают "мыслить" комбинированием команд и токенов, подчас просто пытаясь угадать решение, и в дальнейшем приучаются к такому кривому стилю,

почему бы сразу не обучать операционной семантике (универсально применимой к любой программе)? А от неё совершенно естественный переход будет и к формальным темам (верификация, доказательство корректности, теория типов...).

В TaPL есть несколько главок по такому подходу, я на треке по вычислительным моделям предлагаю лайт-версию этой темки, но вопрос, конечно, риторический... Зачем, когда у всех теперь есть ЖПТ.