Session with the Coq Development Team
summary
Coq announces concrete engineering changes and breaking-but-fixable migration details: 8.10 adds a new prop equality behavior, compact primitive fixed-size integers and better numeral/termination handling; 8.11 brings primitive floating-point numbers, expanded kernel checks and an LTac v2 integration with FFI; a new compile interfaces system enables incremental recompilation; work on persistent arrays, VS Code LSP support, SSReflect tactic improvements, and ~300 PRs from 61 contributors shape upcoming compatibility pain points and migration recipes.
AI-written summary · about
chapters (20)
- 0:00Coq 8.10 release intro
- 2:10Coq 8.11 major features
- 5:16Coq 8.11 release challenges
- 6:25Coq 8.12 expected features
- 10:05Q&A with Mehta update
- 11:38Persistent arrays in Coq
- 13:04VS Code extension status
- 14:50Proof General future
- 16:58Deprecated features handling
- 19:20Ltac1 to Ltac2 migration
- 20:48Lean vs Coq type classes
- 24:30Standard library status
- 26:18FFI and Iris challenges
- 28:47Coercions and inheritance
- 30:34SSReflect vs standard tactics
- 33:47Apply tactic changes
- 37:19MetaCoq future
- 40:13Dune and package managers
- 41:19Universe indices with notations
- 42:08Closing remarks
related talks
46mSession with the Coq Development Team
42mSession with the Rocq Development Team
54m10-Year Most Influential Paper Talk: Coq: the world's best macro assembler?
42mMetaCoq as a tool to prevent future unsoundness in Coq
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mInterpreting OCaml GADTs into Coq
23mVellvm: Formalizing the Informal
15mCompiling with Continuations, Correctly