问题描述
有一种编程“风格”（或者可能是范式，我不知道该怎么称呼它）如下：
首先，您编写规范：对您的（整个或部分）程序要做什么的正式描述。这是在编程系统内完成的；它不是一个单独的工件。
然后，您编写程序，但是 - 这是这种编程风格与其他风格之间的主要区别 - 此编写任务的每一步都以某种方式由您编写的规范指导在上一步中。这种指导究竟如何发生变化很大；在 Coq 中，您有一种元编程语言 (Ltac)，它可以让您在幕后构建实际程序的同时“细化”规范，而在 Agda 中，您通过填充“漏洞”来编写程序（我实际上不确定它是如何进入的） Agda，因为我最习惯使用 Coq）。
这并不是每个人都喜欢的编程风格，但我想尝试用通用的、流行的编程语言来练习它。至少在 Coq 中，我发现它相当容易上瘾！
...但是我什至如何在证明助手之外寻找方法来做到这一点？这就引出了一个问题：我正在为这种编程风格寻找一个名称，以便我可以尝试查找可以让我在其他编程语言中进行类似编程的工具。
请注意，当然更合适的问题是直接询问此类工具的示例，但询问答案列表的 AFAIK 问题不适用于 Stack Exchange 站点。
而且要明确的是，我并没有那么希望我真的会找到很多东西；这些主要是学术消遣，您的典型编程语言并不真正适合这种编程风格（例如，规范语言可能最终变得非常复杂）。但值得一试！
解决方法
它被称为证明驱动开发（或类型驱动开发）。但是，关于它的信息很少。
,您提到的通过 ltac（在 coq 的情况下）或孔（在 Agda 和 Idris 的情况下）缓慢创建程序的过程称为细化。因此，您还可以在文献中找到这种风格的参考资料，作为通过细化或通过细化编程的证明。
现在要意识到的最重要的事情是，这种编程风格是更复杂的类型系统所固有的，它将允许您从当前环境中提取尽可能多的信息。所以很自然的发现附加依赖类型，虽然不一定如此。
正如在另一个回复中提到的，您还将找到对它作为类型驱动开发的引用，有一个关于它的 idris book。
您可能有兴趣研究其他一些项目，例如 Lean、Isabelle、Idris、Agda、Cedille，以及 Liquid Haskell、TLA+ 和 SAW。
,正如前两个答案所指出的，您提到的程序风格的可能名称当然是：类型驱动开发。
从 Coq 的角度来看，您可能对以下两个参考文献感兴趣：
Certified Programming with Dependent Types（CPDT，Adam Chlipala 着）：一本 Coq 教科书，教授开发依赖类型 Coq 理论和自动化相关证明的高级技术。
-
经验报告：Coq 中认证树算法的类型驱动开发（作者：Reynald Affeldt、Jacques Garrigue、Xuanrui Qi、Kazunari Tanaka），发表于 Coq Workshop 2019（ slides、extended abstract)：
作者还使用首字母缩写词 TDD，有趣的是，它在软件工程社区中还有另一个接受：test-driven development（这种广泛使用的方法自然会导致高质量的测试套件）。
实际上，TDD 的两种接受都有一个共同的想法：首先系统地编写（所考虑单元的）规范，然后才编写一些满足规范的代码（使单元测试通过），然后我们循环并递增指定+实现（+重构）其他代码单元。
最后但并非最不重要的是，this discussion from the Discourse OCaml forum 中有一些额外的指针。