Добро пожаловать на подфорум “Rocq на русском языке”!
Rocq – это компьютерная система для работы с формальными доказательствами, основанная на теории типов. Первые версии Rocq были написаны около 1983 года в исследовательском институте Inria, Франция.
Rocq использовался для нескольких новаторских проектов, например, верифицированного компилятора с языка Си CompCert, формальных доказательств теоремы о четырёх красках и теоремы Фейта – Томпсона.
Этот раздел форума предназначен для всех тех, кто хотел бы обсудить Rocq или задать вопросы о нём на русском языке.
У данного подфорума отсутствует конкретная тема или направление – приветствуются любые вопросы или комментарии. Однако, стоит помнить, что, как это принято в мире научных исследований, основная часть дискуссий о технически сложных моментах обычно происходят в англоязычной части форума.
Правила русскоязычного подфорума определяются кодексом поведения проекта Rocq. Краткое резюме правил – уважение, взаимопомощь и непринуждённая атмосфера 
.