The Rocq proof assistant

Overview of Rocq as a programming language and theorem prover.