Прекрасное, дико уважаю:

"Фундаментальная математика — теория всего в IT и не только. Теория типов и формализация в Coq"

Такой уровень и есть наша примерная цель. Делаю постепенно курс по HoTT для программистов, и курс "Ясные системы" (как быстро и легко писать простой и понятный код систем ultra-larfe-scale), этой весной постараюсь сосредоточиться только на этом.

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

fun f(x: X) {...}
fun f(y: Y) {...}
fun f(z: Z) {...}

вы тут же бросаетесь его переписывать с помощью контекстных ресиверов:

context(Specifics<T>) fun <T>f(a: T){...}

Но даже если и без завтипов, видна аналогия с тайп-классами, linear types, имплицитными параметрами, effect systems из ФП.

В котлине конечно классно это сделано; трейты в Rust?
Так то даже в F# придётся помучиться:

let f<'T when 'T :> ContextHandler<'T>> (a: 'T) =
.... let context = Activator.CreateInstance<'T>()
.... (context :> ContextHandler<'T>).Handle(a)

А вот питон как всегда красавчик )))

@ contextmanager
def context():
print("Начало контекста")
yield
print("Конец контекста")

with context(): print("Работа внутри контекста")