Исследователи формализовали подмножество архитектуры x86 в Coq, сделав его "лучшим макро-ассемблером". Используя dependent types, type classes и notation, они упростили барочную семантику x86 до компактной формы. Биты, байты и память моделируются конкретными функциями, вычислимыми в Coq; они маппятся на математические объекты SSREFLECT (натуралы, целые по модулю 2^n). Ассемблер поддерживает привычный синтаксис (как в MASM), включая лексически-ограниченные метки, и генерирует hex-байты. Обычные определения Coq служат макросами для условных операторов, циклов, локальных переменных и процедур с параметрами. Доказана теорема корректности, связывающая машинный код с формулой separation logic для верификации.

Пример — код вычисления факториалов 10 (3628800) и 12 (479001600) с выводом через printf из MSVCRT.DLL. Макросы вроде call_cdecl3 (для cdecl-вызова), while и letproc скрывают детали. Ассемблируется в hex: EB 1A B8 01 00 00 00.... Coq генерирует PE-файл "winfact.exe" для Windows, исполняемый нативно. Поддержка bare metal возможна.

• Обсуждение бумаги о Coq как "лучшем макро-ассемблере" для доказательства семантики ассемблерного кода в safety-critical системах (авто, авиация).
• Участники делятся опытом: компилятор в Coq за неделю, верификация F-16, переименование в Rocq, ссылки на HN и PDF.
• Вопросы о синтаксисе, доказательстве блоков asm-кода, подмножестве x86-инструкций; критика feature creep и сравнения с Lisp/Prolog.
• Мнения: Coq упрощает rigor, Lisp позволяет имитировать, но не "с лёгкостью"; сомнения в практической верификации сложных систем.

Cuq — это фреймворк, преобразующий MIR (промежуточное представление Rust) в Coq для формальной семантики и верифицированного перевода Rust-ядер GPU. Проект нацелен на PTX (язык ассемблера NVIDIA) и обеспечивает математически строгую основу для GPU-программирования на Rust.

Фреймворк позволяет формально доказывать свойства GPU-кода и обеспечивает верифицированный перевод из Rust в PTX. Это критически важно для безопасности и надежности вычислений на GPU, где ошибки могут иметь серьезные последствия. Cuq заполняет пробел между высокоуровневым Rust-кодом и низкоуровневым GPU-исполнением, предоставляя формальные гарантии корректности преобразований.

• Проект, который переводит MIR Rust в Coq для формальной верификации ядра CUDA, вызвал бурную дискуссию из-за имени «cuq».
• Участники спорят, звучит ли название как «кук» или «кью-кью»; критика имени превратилась в обсуждение культурных различий.
• Некоторые предлагают переименовать проект в «rocuda», «rocq» или «rocq», чтобы избежать нежелательных коннотаций.
• Автор отвечает, что имя строится на словах CUDA и Coq, и что он не осознавал двусмысленность; вопрос о переименовании остаётся открытым.
• Несмотря на спор, техническая ценность проекта в том, что он может формально верифицировать параллельные вычисления и уменьшить гонки за счёт формального доказательства корректности.

Определение пятого значения функции занятого бобра

Авторы: Коллаборация bbchallenge (Джастин Бланшар и др.)

Аннотация: Мы доказываем, что $S(5) = 47,176,870$ с использованием системы проверки доказательств Coq. Значение занятого бобра $S(n)$ — максимальное число шагов, которое машина Тьюринга с $n$ состояниями и 2 символами может выполнить с нулевой ленты до остановки. Функция $S$ была введена Тибором Радо в 1962 году как один из простейших примеров невычислимой функции. Доказательство включает перебор $181,385,789$ машин Тьюринга с 5 состояниями и определение для каждой из них, останавливается ли она. Наш результат — первое определение нового значения занятого бобра за более чем 40 лет и первое формально верифицированное значение, что демонстрирует эффективность массовых онлайн-исследований (bbchallenge$.$org).

Комментарии: 48 страниц, 17 рисунков

Предметные области: Логика в информатике (cs.LO); Формальные языки и теория автоматов (cs.FL); Логика (math.LO)

Цитирование: arXiv:2509.12337 [cs.LO]

• Результат BB(5) был подтверждён с использованием комбинации исчерпывающего перебора и продвинутых методов анализа (десидеров) для проверки остановки машин Тьюринга.
• Процесс проверки был значительно оптимизирован: большинство машин было отсеяно на ранних этапах, и лишь 183 машины потребовали глубокого моделирования (до 47 млн шагов).
• Исследование является крупным collaborative-проектом с открытым исходным кодом, аналогичным другим сообществам, изучающим клеточные автоматы и гугологию.
• Значение BB(5) само по себе не имеет прямого практического применения и считается чисто академическим достижением, однако разработанные методы могут быть полезны для статического анализа программ и решения проблем остановки.
• Некоторые машины Тьюринга, включая кандидата для BB(6), выполняют вычисления, аналогичные последовательности Коллатца, что представляет отдельный математический интерес.
• Проверка доказательства с помощью Coq требует нескольких часов на обычном компьютере, что несопоставимо с вычислительными затратами на его получение.
• Для машин с большим числом состояний (начиная с BB(6)) прямое вычисление значения считается невозможным из-за его колоссального размера и неразрешимости проблемы остановки в общем случае.