coq - 规范语言与编程语言

Question

这是一道基础题。 Coq 有一种 Gallina 形式的规范语言。根据我的理解，Coq 本身是用 OCaml 编写的。

我的问题是，Gallina 什么时候上场？它的用途是什么？为什么？我想我误解了规范语言与编程语言的使用。

Answer 1

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

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

现在，Coq 系统(类型检查器、编译器、IDE 等)是使用 OCaml 作为构建语言和工具的编程语言构建的。但就像其他编程语言一样，语言和工具的实现方式在语言中几乎不应该是可见的:无论是自托管、使用 C 构建、汇编还是其他，在某种程度上都是一个实现细节。

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