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

В России тех, кто применяет продвинутые практики computer science (например ФП), оптимистично, наверное сотни (в Европе и США на порядки больше, там целые институты этим занимаются), и таковых всё меньше. Всё, что они делают, это существенно улучшают программные системы на фоне всех остальных. Можно без них обойтись? Безусловно.

Может ли здесь теоретически возникнуть некая критическая масса, которая окажет качественное влияние на всё ИТ? Вряд ли, потому что если не возникла на Западе ранее, то теперь уже тем более. Но зато, теперь 10% "лучших" разработчиков (оценка Jellyfish) потребляют примерно 380 млн токенов в месяц. Теперь это новая айтишная илита :)

И тем не менее, я продолжаю тратить много времени на размышления о формальных методах (потому что именно они источник почти всего моего дохода:). Но при этом я не делюсь большинством деталей, потому что 98% ребят, изучающих эти темы, не используют ФМ активно и напрямую, да и никогда не будут использовать. Поэтому я стараюсь упаковывать эти темы в формате СильныхИдей, ФункциональныхАрхитектур, треке HoTT и LPF (по возможности в формате ELI5 / explain like I'm 5 years old), дабы не терялась связь с повседневной практикой.

Например, идея "силы свойства" означает, что некоторые тесты более эффективны, чем другие.

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

Или почему автоматное программирование это "гомоморфизм из пр-ва состояний в зависимую сумму (в крайнем случае произведение) управляющего и вычислительного пр-в" (не моё:), и что крайне полезное из этого следует (в частности, везде где только есть такая возможность (т.е. почти везде), реализуйте логику как автомат, что легко формализуется спеками и тестируется).

Или почему программисты практически никогда не рассуждают о коде с т.зр. минимального доказательства его корректности, что избавило бы от 98% логических багов.

И т.д.