Математика как майнинг благодати?

При чтении всего этого складывается впечатление, что математики всерьёз не понимают прозаических оснований сего мира.

Математика внутри себя считает "чистые", самые абстрактные, области своим наивысшим достижением, пиком прогресса и главным показателем развития. Теория категорий, математическая логика, теория множеств, теория типов – всё это и многое другое парит над прикладными областями, слегка на них поплёвывает с высоты и посмеивается, считая себя свободной от мирских ограничений, ведомой эксклюзивно особым эстетическим чувством, которое врождённо присуще топовым талантливым математикам.

Зачем нужна, скажем, теория категорий? С одной стороны это набор "паттернов разработки" математических теорий, такая метаматематика. С другой стороны разработчики теорката, формализуя красивые узоры из платоновских сфер, выступают как бы майнерами некоего космического блокчейна, токены в котором вызывают прирост благодати человечества.

Говоря прозаически – абстрактные построения являются произведениями искусства. Точно также как картины, музыка, художественная литература. Радуют коллег с развитым вкусом, широкие слои населения с эстетической интуицией (открытые лекции по самым заковыристым дисциплинам всегда сотни слушателей собирают) и, стоит надеяться, Господа Бога.

При этом чувствуется так, как будто теоретическим математикам повезло, что им платят не за какой-то конечный продукт, а по сути за то что они классные ребята – за благодать, за талант.

А какой, кстати, конечный продукт теорката – не ракеты же с его помощью запускать?

Т.е. всем ясно, что дифференциальные уравнения нужны исключительно для того, чтобы запустить Старлинк в космос; теория графов чтобы Старлинк эффективно организовать в сеть; линейная алгебра чтобы Старлинк эффективно передавал сигналы и т.п. На это выделяются гранты, гранты осваиваются математиками-прикладниками и инженерами, Старлинк работает.

А теория категорий для чего?

Не поверите – для того, чтобы у Старлинка софт был без багов. Теория категорий поддерживает теорию типов, теория типов служит основой для систем дедуктивной верификации, эти системы используются для доказательства корректности программ.

Буквально теоркатом запускают ракеты в космос и буквально на те же военные деньги его развивают.

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