Talos не разделяет код, который запускает WebAssembly, и код, который описывает её правила. В одном репозитории на Lean 4 одни и те же определения выполняют Wasm-инструкции и служат основой для рассуждений о них. Это значит, что спецификацию не нужно синхронизировать с реализацией отдельно: если интерпретатор что-то проглотил, с ним можно рассуждать формально, не подгоняя спецификационный интерпретатор под код. Пока проект в активной разработке, API доказательств может меняться, но сам подход цепляет. Код лежит на GitHub.
Интерпретатор Wasm, который одновременно доказывает свою правоту
Talos не разделяет код, который запускает WebAssembly, и код, который описывает её правила. В одном репозитории на Lean 4 одни и те же определения выполняют Wasm-инструкции и служат основой для рассуждений о них.
Это значит, что спецификацию не нужно синхронизировать с реализацией отдельно: если интерпретатор что-то проглотил, с ним можно рассуждать формально, не подгоняя спецификационный интерпретатор под код. Пока проект в активной разработке, API доказательств может меняться, но сам подход цепляет.
Код лежит на GitHub.
