# О категории "Coq на русском"

**URL:** <https://discourse.rocq-prover.org/t/coq/161>\
**Category:** \[ru\] Rocq на русском\
**Created:** [February 26, 2019, 9:14pm UTC](https://discourse.rocq-prover.org/t/coq/161 "2019-02-26T21:14:29Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![anton-trunov](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/anton-trunov/32/54_2.png) [@anton-trunov](https://discourse.rocq-prover.org/u/anton-trunov)\
**Post date:** [February 26, 2019, 9:14pm UTC](https://discourse.rocq-prover.org/t/coq/161/1 "2019-02-26T21:14:29Z")

</div>

Добро пожаловать на подфорум “Rocq на русском языке”!

Rocq – это компьютерная система для работы с формальными доказательствами, основанная на теории типов. Первые версии Rocq были написаны около 1983 года в исследовательском институте Inria, Франция.

Rocq использовался для нескольких новаторских проектов, например, верифицированного компилятора с языка Си CompCert, формальных доказательств теоремы о четырёх красках и теоремы Фейта – Томпсона.

Этот раздел форума предназначен для всех тех, кто хотел бы обсудить Rocq или задать вопросы о нём на русском языке.

У данного подфорума отсутствует конкретная тема или направление – приветствуются любые вопросы или комментарии. Однако, стоит помнить, что, как это принято в мире научных исследований, основная часть дискуссий о технически сложных моментах обычно происходят в англоязычной части форума.

Правила русскоязычного подфорума определяются кодексом поведения проекта Rocq. Краткое резюме правил – уважение, взаимопомощь и непринуждённая атмосфера 🙂.