...Ну а единичное количество топовых программистов, которых всякая шушера типа Цукера будет хантить за миллиарды долларов, лучшие универы будут учить уже даже не столько программированию, сколько тому, как формально доказывать правильность кода.

Например, ООП. Перед обучением cперва разберём, почему класс -- это, по сути, жалкая попытка перенести в программирование подходы категоризации из когнитивной психологии. Категории в нашем уме -- это "размытые" конструкции, и ООП оказалось таким удачно продаваемым подходом, что класс -- это формализованная, "обрезанная" категория.

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

Тут хорошо бы сперва купить у меня побольше курсов пройти "как понять в programming in small всё", где разбираем исторические корни ООП и его место в десятках других подходов, затем мой гайд по объектной вычислительной модели, после чего, надеюсь, будет хорошее понимание и концептуальной структуры ООП, и более сильных подходов.
(Какой ещё полиморфизм в ООП? Смешно. Так, детский лепет...)

Потом трек по ООАП, где получаем наивную формализацию ООП через абстрактные типы данных, включая понимание концепции модулей. Но делаем задания по реальному "объектному" кодингу только на чистом С++ (потому что множественное наследование и дружественные функции), а потом на его темплейтах.

Ну и наконец изучаем взрослую формализацию ООП в теорем-прувере Lean (или на моей реализации HoTT).