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

...есть один русскоязычный полуживой чятик по формальным методам, где админ с поехавший кукухой (сам так говорит), 50% работают в европейских профильных структурах типа INRIA (потому что европейская школа computer science абсолютный топчик, Америка сильно остаёт), а 48% мечтают туда свалить после PhD, для чего старательно выискивают подходящие темки, как бы опубликоваться в международных академических изданиях и засветиться на научных конфах.

При этом я даже лично знаю несколько человек, теперь уже полностью "с противоположной стороны баррикад", кто их старательно и успешно к себе сманивает.

Ну и изучают они соответственно западные теорем-пруверы вроде Rocq и англоязычные гайды, и ни о каком развитии этой темки в России конечно речь уже давно не идёт, это я как-то ещё шевелюсь...

...И о медалях-орденах ты помышлять не моги:
Всего награды -- только знать наперёд,
Что по весне споткнётся кто-то о твои сапоги
И идиотский твой штандарт подберёт.