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 basictacticsthat 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.