As I understand, Gallina is the “programming language” embedded in Coq (that one can write proofs later which are checked using the formal system CIC Calculus of inductive constructions):
The first half of this chapter introduces the most essential elements of Coq’s native functional programming language, called Gallina . The second half introduces some basic tactics that can be used to prove properties of Gallina programs.
reference: https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
LTac seems to be a functional programming language for manipulating goals (what in my head I call coq terms) using tactics (or custom tactics).
My questions are (numbered to make it easier to address):
- why do we need two different languages inside of Coq and not have everything be in a single unified language?
- Is the main difference between Gallina vs LTac? Is the main difference that one is a language to express native programs in Coq while the second to create custom tactics?
- is a proof script proving something about a coq term or a Gallina program in Gallina or LTac? (what is the language of proof scripts essentially)
- Is this sort of a good approximation of Coq?
Coq = Gallina (for programming) + Ltac (for tactics) + CIC (for formal system e.g. type system, judgments, etc)
- Are Coq terms in Gallina or something else?
Context: I am transitioning from Isabelle to Coq and it seems everything in Isabelle is “one single language” (which makes sense if one reads its history coming from LCF https://en.wikipedia.org/wiki/Logic_for_Computable_Functions ) and I am trying to wrap my head around what exactly “is Coq”. Perhaps I shouldn’t be comparing it to what I am already used to but it seemed natural to try to compare them. In particular, perhaps this was true in Isabelle too, but I still can’t form a stable model in my head of what an evolving grammar that is not fixed means.