Но если есть идеи лучше в этом направлении, буду рад послушать

Ну, например, подмножество LLVM IR :)

Я думал в этом направлении тоже.

Но к выводам не пришёл пока.

Первая мысль была что подавать и этот уровень и типизацию это достаточно много

Всё-таки это инструмент для компиляторов

А я и подразумеваю программу для будущих компиляторщиков и прочих строителей инструментального ПО. Выше много было дельного сказано об образовании программистов, но, почему-то, все подразумевали какого-то абстрактного разработчика, без какой-либо специализации. При этом специализацию эту легко извлечь уже из конкретных советов участников дискуссии. Вот Вы, например, хотите готовить будущих специалистов по верификации ПО :)

Good point.

мне кажется что понимание алгоритмов, их верификация (так или иначе — тесты, модели или даже доказательства) это достаточно важная часть инструментария программистов в ближайшие 10-20 лет

софта все больше, и сильно лучше он пока что не становится

но потихоньку сдвиг в ту сторону (анекдотически) наблюдается

Время покажет, да или нет

Ближайшие 10-20 лет?! Да Дейкстра призывал с этого начинать ещё 40 лет назад! 😄

с чего этого?

Уверен, уже тогда ему тыкали "им же на работу нужно устраиваться!" 😂

Что именно "с чего это?"

призывал с чего начинать?

С верификации. Призывал начинать обучение программированию с верификации.

И ещё троллил чтобы первый год к компьютеру студентов не подпускали, чтобы на бумажке всё программировали. 😄

а ведь так было совсем недавно