Coq: A program specification and mathematical higher-level language (coq.inria.fr)

Coq 8.11.0 was recently released: https://github.com/coq/coq/releases/tag/V8.11.0

This version introduces a new tactic language, Ltac2.

Dozens of previous threads: https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...