Типичный программист | IT, программирование, разработка, ИИ

IT и технологии · 20 июня 2026 г.

Открыть канал в MAX

Интерпретатор Wasm, который одновременно доказывает свою правоту — 20 июня 2026 г. в 12:28:39.358

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