Без заголовка

Тут видимо все очень зависит от роли/целей. Я "осторожно" предполагаю, что Вам оно в основном нужно, чтобы заявить клиентам/подопечным "используйте вот эту штуку, это типа круто и полезно". Посему должен быть достаточно высокий степень зрелости. Мне это нужно потому что я хочу использовать в реальных/промышленных проектаъ, и получить от этого пользу (получить более надежный софт, найти баги/проблемы, снизить затраты на достижение того или иного уровня качества). Лет 10 назад уже были проекты где это было ограниченно полезно (фин софт в моем случае), но все же затраты на это дело слишком велики (слишком сырые тулзы). Дорабатывать тулзы я не мог. Сейчас тулзы улучшились, и я нашел сферу, где формальные методы гораздо более актуальны (впрочем это все тот же финсофт :)). Посему для меня сейчас оптимальный момент этим заниматься (чтобы быть готовым к тому когда через 10 лет тут будет бурный рост). Ну и еще один аспект - в зависимости от целей, нам нужна разная степень крутости формальных методов. А значит и потребная выразительность ЯП разная. Для большинства применений хватит Скала, C# наверное тоже (не очень с ним знаком) ну и других языков на которых удобно делать eDSL (Haskell, Groovie, etc). Иногда даже крутой поддержки DSL не нужно. Я бы к примеру сейчас вместо Скалы начал с Котлин - это если в Жаба мире, ну и C# уверен не хуже. Потому что начинать лучше все равно с простых формальных методов, там где депендент типов особо не видно еще :). Но вот на перспективу их хочется иметь все равно :). Поэтому в отдаленной перспективе интересны подходы к метапрограммированию типа Lean Prover. Мне пока видятся такие направления (сугубо с моей колокольни): - онтологии как инструмент моделирования предметной области, с целей понимания требования, выявления противоречий и генерации базового кода из этих моделей - модели дизайн уровня, т.е. уточнение моделей предметной области, как они мапятся на всякие архитектуры/структуры и проч. В том числе протоколы. Выявление проблем (багов). - низкий уровень - генерация тестов, верификация программ Мне думается что суровые вещи типа депендент тайпс нужны преимущественно на нижнем уровне. Хотя всякие протоколы - это тоже круто, но там наверное можно без dependent types жить.