规范语言vs编程语言

Question

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

我的问题是，Gallina什么时候开始发挥作用？它是用来做什么的，为什么？我想我误解了规范语言和编程语言的使用。

Answer 1

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

在某些校对助手中，用来构建程序的语言与用来构建规范的语言是分开的，而用来构建校样的语言甚至可以是第三种语言！在Coq中，您可以使用Gallina完成所有这三个任务，因为它使用了一个支持所有这些任务的统一框架。

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

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

Answer 2

对于普通用户来说，Coq是用OCaml编写的，这一事实是不可见的。Gallina是Coq的语法。(它并不是所有的语法，还有像策略语言之类的东西。)如果您使用Coq编写程序，则可以使用Gallina语法编写它。当然，Coq并没有将证明和程序的概念分开(这就是Curry-Howard同构的全部要点，证明和程序是一回事)。