CODEWITHSUNDEEP
coqformal-languages
deedee96
deedee96

Reputation: 39

Specification Language vs Programming Language

This is a basic questions. Coq has a specification language in the form of Gallina. From my understanding Coq itself is written in OCaml.

My question is, when does Gallina come into play? What is it used for and why? I think I misunderstand the use of specification languages vs programming languages.

Upvotes: 2

Views: 997

Answers (2)

Ptival
Ptival

Reputation: 9437

Gallina is both the "programming language" and the "specification language" of Coq.

In certain proof assistants, the language with which you build your programs is a separate one from the language in which you build your specifications, and the language in which you build your proofs could even be a third language! In Coq, you are able to use Gallina for all three of these tasks, because it uses a unifying framework that supports all those endeavors.

Now, the Coq system (the type-checker, the compiler, the IDE, etc.) is built using OCaml as the programming language for building the language and tools. But just like other programming languages, how the language and tools are implemented should almost never be visible within the language: whether it is self-hosted, built using C, assembly, or what not, is an implementation detail to some extent.

OCaml does come up in some advanced uses of Coq (if you want to write plug-ins), but for the most part, you can just think of it as the "assembly" that runs your proof assistant.

Upvotes: 10

Perry
Perry

Reputation: 4495

To a normal user, the fact that Coq is written in OCaml is invisible. Gallina is Coq's syntax. (It isn't all of it's syntax, there's stuff like the tactic language etc.) If you write a program in Coq, you write it in the Gallina syntax. Of course, Coq does not separate the notion of proofs and programs (that's the whole point of the Curry-Howard Isomorphism, that proofs and programs are the same thing.)

Upvotes: 2

Related Questions