Coq: The world’s best macro assembler

Используем популярный пруф-ассистант как мощный макроассемблер. Всё от моделирования архитектуры до генерации бинарного кода и его верификации делается внутри Coq.
Исполняемость модели внутри Coq (можно "выполнять" инструкции и видеть состояние).
Повторное использование формализованной математики (SSReflect, ATBR).
Горизонтальная композиция DSL — возможность комбинировать предметно-ориентированные языки внутри Coq.
Всё в одном месте: модель, код, спецификации, доказательства, с полным контролем корректности и возможностью повторного использования формальных теорий.