依赖类型(例如Coq或Agda)启用的编程风格的名称是什么？

Question

有一种编程“样式”(或者范式，我不知道该如何称呼它)如下所示：

首先，编写一个规范:对(整个或部分)程序所要做的事情进行正式描述。这是在编程系统中完成的；它不是一个单独的工件。

然后，编写程序，但是--这是这种编程风格和其他编程风格之间的关键区别--这个编写任务的每一步都在某种程度上由您在前一步中编写的规范所指导。这个指导是如何发生的?在Coq中，您有一种元编程语言(Ltac)，它允许您在幕后构建实际程序的同时“细化”规范，而在Agda中，通过填充“漏洞”(我不确定它在Agda中是如何进行的，因为我主要习惯于Coq)来编写程序。

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

...but，我怎么才能在证据助手之外寻找方法呢？这就引出了一个问题:我正在为这种编程风格寻找一个名字，这样我就可以尝试查找一些工具，让我可以用其他编程语言那样编程。

当然，更恰当的问题是直接询问此类工具的示例，但是AFAIK问题询问答案列表并不适合于Stack Exchange站点。

而且要明确的是，我并不完全希望我能找到很多东西；这些都是学术上的消遣，而您典型的编程语言实际上并不适合这种编程风格(例如，规范语言可能最终会变得非常复杂)。但值得一试！

Answer 1

它被称为验证驱动开发(或类型驱动开发)。然而，有关这方面的信息很少。

Answer 2

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

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

正如在另一个响应中提到的，您也会发现对它的引用是类型驱动的开发，有一个关于它的伊德里斯书。

你可能对其他一些项目感兴趣，如精益，伊莎贝尔，伊德里斯，Agda，雪地，也许液体Haskell，TLA+和SAW。

Answer 3

正如前面的两个答案所指出的，您提到的程序风格的一个可能名称是:类型驱动开发。

从Coq的角度来看，您可能对以下两个引用感兴趣：

• 具有依赖类型的认证编程(CPDT，由Adam编写)：一本Coq教科书，它教导高级技术发展可靠类型的Coq理论和自动化相关的证明。
• 经验报告: Coq中认证树算法的类型驱动开发(由雷纳德·阿弗莱特、雅克·加里格、齐宣瑞、田中和里)，发表在Coq 2019讲习班 (幻灯片，扩展抽象)上： 作者还使用了首字母缩略词TDD，有趣的是，在软件工程社区中也有另一个词：https://en.wikipedia.org/wiki/Test-driven_development (这一广泛使用的方法自然导致了高质量的测试套件)。 实际上，对TDD的两种接受都有一个共同的想法:一个系统地从编写规范(考虑的单元)开始，然后才编写一些满足规范(使单元测试通过)的代码，然后循环并递增地编写specify+implement(+重构)其他代码单元。

最后但并非最不重要的一点是，来自语篇OCaml论坛的讨论中有一些额外的指针。