1

有一种编程“风格”（或者可能是范式，我不知道该怎么称呼它）如下：

首先，您编写规范：对您的（整个或部分）程序要做什么的正式描述。这是在编程系统内完成的；它不是一个单独的工件。

然后，您编写程序，但是——这是这种编程风格与其他风格之间的关键区别——这个写作任务的每一步都以某种方式受到你在上一步中编写的规范的指导。这种指导的具体发生方式千差万别；在 Coq 中，你有一种元编程语言 (Ltac)，它可以让你在幕后构建实际程序的同时“改进”规范，而在 Agda 中，你通过填充“漏洞”来编写程序（我实际上不确定它是如何进入的Agda，因为我主要习惯于 Coq）。

这并不是每个人都喜欢的编程风格，但我想尝试用通用的、流行的编程语言来练习它。至少在 Coq 中，我发现它相当容易上瘾！

...但是我什至如何在证明助理之外寻找方法呢？这就引出了一个问题：我正在为这种编程风格寻找一个名称，以便我可以尝试查找可以让我在其他编程语言中进行类似编程的工具。

请注意，当然更合适的问题是直接询问此类工具的示例，但要求答案列表的 AFAIK 问题不适合 Stack Exchange 站点。

需要明确的是，我并不是那么希望我真的会找到很多；这些主要是学术消遣，而您的典型编程语言并不真正适合这种编程风格（例如，规范语言最终可能会变得难以置信地复杂）。但值得一试！

4

3 回答 3

0

您提到的通过 ltac（在 coq 的情况下）或孔（在 Agda 和 Idris 的情况下）缓慢创建程序的过程称为细化。因此，您还可以在文献中找到这种风格的参考，作为细化的证明或细化的编程。

现在要意识到的最重要的事情是，这种编程风格是更复杂的类型系统所固有的，它将允许您在当前环境中提取尽可能多的信息。因此很自然地发现附加依赖类型，尽管不一定如此。

正如在另一个回复中提到的，您还将找到对它作为类型驱动开发的引用，有一本关于它的idris 书。

您可能有兴趣研究其他一些项目，例如 Lean、Isabelle、Idris、Agda、Cedille，也许还有 Liquid Haskell、TLA+ 和 SAW。

于 2021-01-05T23:08:38.077 回答
0

正如前两个答案所指出的，您提到的程序样式的一个可能名称当然是：类型驱动开发。

从 Coq 的角度来看，您可能对以下两个参考资料感兴趣：

  • Certified Programming with Dependent Types ( CPDT , by Adam Chlipala)：Coq 教科书，教授高级技术来开发依赖类型 Coq 理论和自动化相关证明。

  • 经验报告：Coq 中认证树算法的类型驱动开发（Reynald Affeldt、Jacques Garrigue、Xuanrui Qi、Kazunari Tanaka），发表于Coq Workshop 2019（幻灯片，扩展摘要）：

    作者还使用了首字母缩略词 TDD，有趣的是，它在软件工程社区中也有另一种接受：测试驱动开发（这种广泛使用的方法自然会产生高质量的测试套件）。
    实际上，两种对 TDD 的接受都有一个共同的想法：一个系统地从编写规范开始（考虑的单元），然后才编写一些满足规范的代码（使单元测试通过），然后我们循环并增量指定+实现（+重构）其他代码单元。

最后但并非最不重要的一点是，Discourse OCaml 论坛的讨论中有一些额外的提示。

于 2021-01-05T23:57:11.463 回答
0

它被称为证明驱动开发（或类型驱动开发）。但是，关于它的信息很少。

于 2020-12-31T06:49:15.587 回答