Coq Platform2025.01.0

Coq Platform позволяет пользователям писать формальные спецификации и создавать доказательства, которые проверяет компьютер, устраняя необходимость математических и программных рассуждений с точными, проверенными машиной результатами. Это формальная система управления доказательствами, построенная вокруг Rocq Prover, интерактивного теоремы и языка программирования с зависимой типизацией для механизированного рассуждения.

Его экспрессивная система типов и язык доказательств могут проверять программы на соответствие строгим спецификациям и поддерживать математические разработки с помощью Curry. Связь Говарда между логикой и вычислениями. Приложения варьируются от проверенных моделей программного и аппаратного обеспечения до низкоуровневой проверки программ и теории гомотопного типа, с заметным использованием в таких проектах, как математические компоненты и компилятор CompCert. Пользователи могут адаптировать разработки с прицельными обозначениями, принуждениями, классами типов, метапрограммированием, стратегиями доказательства и встроенной логикой домена.

Доказательный движок включает байт-код и нативные шашки преобразования, работающие во время выполнения OCaml, в то время как средства извлечения позволяют верифицированному коду взаимодействовать с программами, написанными на других языках. Он подходит исследователям, преподавателям и разработчикам, работающим над доказательством теорем, формальной математикой, семантикой языка программирования и высоконадежным программным или аппаратным обеспечением.

Информация о выпуске для платформы Rocq 2026.07.0 отмечает, что поддержка native compute была повторно включена с OCaml 5, хотя код, специфичный для архитектуры, означает, что поддержка в настоящее время охватывает только некоторые конфигурации x86.