Hacker GitHub

← All repos

rocq-prover/rocq

View on GitHub ↗ ★ 5,655 OCaml

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

44 mentions on Hacker News by 34 people: 4 stories, 40 comments · first 2014-09-07 · latest 2026-09-05

Mentions per year 44 mentions · busiest year 2021 (13)
20082026
AllStoriesComments NewestTopOldest
  1. ▲ 63
    Coq searches for alternative name
    story by janvdberg · 2021-04-09 · 124 comments
  2. ▲ 1
    Coq 8.11.0 released, featuring new Ltac2 tactic language
    story by TheAsprngHacker · 2020-01-30 · 1 comment
  3. ▲ 2
    Quick Reference and Starter Exercises for Learning Coq
    story by testcross · 2019-08-30 · 0 comments
  4. ▲ 3
    Coq 8.9.0
    story by lelf · 2019-02-12 · 0 comments