Session with the Coq Development Team
summary
Coq releases 8.17–8.19 add concrete features: ability to disable notations locally and use temporary scopes with an underscore, Ltac2 gains arrays, maps and nested-match case compilation, and s polymorphism lets definitions live in Prop/Type/Set to reduce duplication. Platform distributes ~50 packages with binary installers. A verified erasing compilation pipeline (CTIC) now bootstraps Coq, rewrite rules are landing for custom computation, and a rebrand to “Rock” plus VS Code UI work are planned.
AI-written summary · about
chapters (9)
- 0:00Welcome
- 3:46Recent Coq features
- 17:39New notation features
- 25:01Coq platform updates
- 29:21Future roadmap
- 38:22Audience questions and community discussion
- 1:08:40Build systems Q&A
- 1:14:37Domain-specific logics
- 1:22:26Closing Q&A
