Главное, что тестирование проверяет, что программа работает правильно на конкретных тестовых случаях.
Например, можно проверить, что Diffie-Hellman вычисляет общий ключ правильно для фиксированных g, p, a, b.
HoTT -- это доказательство. Оно гарантирует, что программа работает правильно во всех возможных сценариях .
Например, можно доказать, что общий ключ в Diffie-Hellman всегда совпадает, даже если злоумышленник перехватывает сообщения (через Path-типы и HomSpace).
=
Тестирование плохо справляется со структурными инвариантами (например, проверка, что вектор всегда имеет длину n).
Я же могу закодировать такие инварианты в типах:
vector = Pi(domain=int, codomain=lambda n: list, function=lambda n: [0] * n)
=
Тестирование требует ручного написания проверок для каждого случая.
HoTT позволяет использовать автоматические методы (например, SMT-солверы, Z3 с моего курса) для доказательства сложных свойств. Она позволяет моделировать атаки через Path-типы и проверять их невозможность.
Например, можно доказать, что злоумышленник не может создать ложный общий ключ, через Sigma-типы для доказательства корректности шагов протокола.
=
Тестирование работает с конкретными значениями , но не с криптографическими абстракциями . Например, нельзя проверить, что хэш-функция необратима.
HoTT позволяет моделировать криптографические примитивы через зависимые типы. Например, я могу определить тип EncryptedMessage, который гарантирует, что сообщение не может быть декодировано без ключа:
EncryptedMessage = Sigma(domain=str, codomain=lambda m: not is_decodable(m), first=message, second=True)
=
HoTT -- это выход на уровень формальных математических методов , где:
-- cвойства доказываются, а не проверяются;
-- структуры данных и их инварианты моделируются на уровне типов;
-- возможны автоматические доказательства и формальный анализ атак.