Proof writing systems
Table of Contents
- rocq
- acl2
1. TODO discussion with djeis on rocq
- in November 2023: https://discord.com/channels/297478281278652417/505106106649935900/1062784134109466665
- in March 2025: https://discord.com/channels/297478281278652417/377481417334063105/1345913977556832356
talked about:
- vernac v.s. Gallina v.s. LTac
- vernac is short for "vernacular"
- it's a "command language"
- some commands takes Gallina or Ltac expressions
- Gallina is a functional language
- LTac is a metaprogramming language
- it generates Gallina
- vernac is short for "vernacular"
- some specificities of the syntax
- a bit about how Coq represents proof states and goals
- what are tactics in Coq