这是一个基本问题。Coq 具有 Gallina 形式的规范语言。从我的理解 Coq 本身是用 OCaml 编写的。
我的问题是,Gallina 什么时候开始发挥作用?它用于什么,为什么?我想我误解了规范语言 vs 编程语言的使用。
9
Gallina 是 Coq 的“编程语言”和“规范语言”。
在某些证明助手中，用于构建程序的语言与用于构建规范的语言是分开的，而用于构建证明的语言甚至可以是第三种语言！在 Coq 中，您可以使用 Gallina 完成所有这三个任务，因为它使用了一个支持所有这些工作的统一框架。
现在，Coq 系统（类型检查器，编译器，IDE 等）是使用 OCaml 作为构建语言和工具的编程语言构建的。但是，就像其他编程语言一样，语言和工具的实现方式几乎不应该在语言中可见：无论是自托管，使用 C，汇编构建还是其他，在某种程度上都是实现细节。
OCaml 确实出现在 Coq 的一些高级用法中（如果您想编写插件），但是在大多数情况下，您可以将其视为运行证明助手的“程序集”。
2
对于普通用户而言，用 OCaml 编写 Coq 的事实是看不见的。Gallina 是 Coq 的语法。（它不是语法的所有，还有战术语言等）如果您用 Coq 编写程序，则可以用 Gallina 语法编写。当然，Coq 并没有将证明和程序的概念分开（这就是 Curry-Howard Isproofism 的全部意义）。
本站系公益性非盈利分享网址，本文来自用户投稿，不代表边看边学立场，如若转载，请注明出处
评论列表（47条）