-- Сергей Игоревич, но ведь можно и без HoTT доказать соответствие реализации спецификации?

Конечно, и это успешно делается десятилетиями (за многие миллионы долларов :)
Так или иначе, классические основания покрывают >95% задач верификации ПО, включая верификации микропроцессоров или криптопротоколов.

То есть и без HoTT вполне можно доказать полноценную корректность системы. Практически все крупные успешные проекты верификации (коих можно пересчитать по пальцам одной руки :) были выполнены без HoTT, используя классические основания:
- теория множеств (ZFC) в математических доказательствах;
- интуиционистская/логика высшего порядка (HOL) в Isabelle;
- исчисление конструкций (CoC) в Coq/Rocq/Lean.

В CompCert (верифицированный компилятор Си на Coq) корректность доказана относительно формальной семантики Си и ассемблера, без использования унивалентности. В ядре seL4 (Линукс по заказу АНБ) с помощью Isabelle через классическую реляционную семантику гарантированы изоляция процессов и сохранение инвариантов.

Когда же HoTT рвёт все Это как тузик?
1) Когда спецификация содержит гомотопически-инвариантные требования (топология, геометрия, перенос структур между изоморфными представлениями). Например, в классических системах (даже с зависимыми типами!) изоморфные структуры формально различны. А в HoTT унивалентность автоматически отождествляет эквивалентные типы, а транспорт вдоль путей позволяет легко и просто переносить доказательства между ними (всё это подробно разбираю для курсантов).

2) Когда становится технически очевидными ограничения Этих систем -- а таких ограничений сегодня множество, и чем дальше, тем больше, от медленной работы самих программ в реальных задачах до огромных объёмов ручной работы для доказательств эквивалентностей. А перейти с них на HoTT тоже сильно тяжело по самым разным причинам (математика HoTT требует переобучения -- например, по замене равенства на гомотопии).

Другими словами всё Это современное (а на самом деле уже давно легаси и big ball of mud) -- как ньютоновская физика, работающая в весьма ограниченных рамках, а HoTT - как математически обобщённая ТО.