Сколь не изучай гомотопическую теорию типов, в итоге, по закону Годвина, всё равно выходишь на темку постквантовой криптографии :) Нельзя рассуждать о будущем ultra-large-scale систем, если прежде всего в них не будет реализована устойчивость к квантовым атакам. Прежде всего это lattice-based алгоритмы, однако в прошлом годе эталонная реализация (на Си!) механизма инкапсуляции ключей Kyber была скомпрометирована просто потому, что оказалась кривой. Ну немудрено. А компилятор лишь подбавил новых проблем.

Без формального доказательства безопасности и корректности (не только реализации, ну и компилятора и исполнимой части) любой криптографический протокол -- просто красивая идея.

/kino классный сериал сейчас выходит "Опасные числа", очень рекомендую.
204