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

Добавлю два цента в поддержку)) (в чатах не хочу) 1) в F# например есть абстракция "функции как типы данных", что сразу сделало её систему типов потенциально (математически) мощнее чем в Java/C#/... А если добавить к F# что-то типа MLTT, то получится его залифтить до Agda. Это каждый раз качественно новый уровень абстракций (дающий потенциальный выигрыш в компактности/выразительности наверное даже на порядки), но как оптимально использовать хотя бы систему типов Java (Тьюринг-полную саму по себе), да, никто не знает, действуют в основном интуиционистски :) Есть type driven development, но там всё с ориентацией в основном на программистские цели (всё те же выразительность/минималистичность в отношении кода), не на постановочные (моделирование с помощью мощных типов). 2) однозначно "бестиповые языки не выживают", системы типов в современных языках быстро усложняются (в хорошем смысле), поэтому любые попытки использования в программах на таких языках безтиповых, безсхемных форматов данных наподобие JSON, не допускающих статический тайпчекинг, следует считать крайне вредными :) Даже XML куда лучше чем JSON.