规范语言与编程语言

Question

这是一个基本的问题。Coq具有Gallina形式的规范语言。据我了解，Coq本身是用OCaml编写的。

我的问题是，Gallina什么时候起作用？它有什么用，为什么？我想我误解了规范语言和编程语言的使用。

Answer 1

Gallina既是Coq的“编程语言”又是“规范语言”。

在某些证明助手中，用于构建程序的语言与用于生成规范的语言是一种不同的语言，而用于构建证明的语言甚至可能是第三种语言！在Coq中，您可以使用Gallina来完成所有这三个任务，因为它使用了支持所有这些工作的统一框架。

现在，使用OCaml作为用于构建语言和工具的编程语言来构建Coq系统（类型检查器，编译器，IDE等）。但是，就像其他编程语言一样，该语言和工具的实现方式在该语言中几乎绝对不应该看到：它是自托管的，使用C语言生成的，还是汇编语言，或者在某种程度上不是实现细节。

OCaml确实在Coq的某些高级用法中出现过（如果您想编写插件），但是在大多数情况下，您可以将其视为运行证明助手的“程序集”。