Наконец-то возвращаюсь к любимым темкам и функциональным архитектурам!!1

Неформально говоря, вся математика - это логика первого порядка (ZF). В классической математике по сути мыслят в теории множеств, в одной из моделей, и поэтому часто у программистов, даже с хорошо прокаченным рациональным мышлением, с математикой возникают проблемы, так как программисты мыслят подсознательно в теории типов и, по большому счёту, в логиках более высоких порядков.
А ежели двигаться в software design из ZF, то мы быстро упрёмся в Гёделя (неразрешимость проверки доказательств).

При этом есть качественное отличие: даже если мы добавим AC, всё равно ZFC неконструктивна. Поэтому спасти программистов на высших уровнях просветления могут только MLTT/HoTT/CTT и, в принципе, эти теории для них естественны по определению. А вот математикам нужна промежуточная тропинка к этому -- от теории множеств через теоркат ETCS или конструктивщину CZF.

Вспоминаем соответствие Карри-Ховарда: нам не нужна квантификация по всем подмножествам, а только по типам (System F). Нафиг нам не нужна неразрешимая логика 2-го порядка, мы прекрасно живём в разрешимых кусочках FOL+ZFC или SOL: классическая функциональщина, а тесты по сути -- это ручная проверка вывода в SOL.

Как из этих рассуждений мы попадаем в формализацию DDD, расскажу дальше.