Rocq is a mature, dependently-typed functional programming language and interactive theorem prover. Learn more about its rich history.