合并(Coq + MetaOCaml) -为什么要放弃？

Question

在窃听OCaml邮件列表上的人之前，我想我应该在这里发布我的问题。我刚刚发现了这个beauty (到Concoqtion网站的链接)。Concoqtion是MetaOCaml的一个扩展，它允许索引类型(可能还有更多)。有了它，可以很容易地创建包含列表长度的列表：

type ('n:'(nat),'a) listl =
   | Nil : ('(0),'a) listl
   | Cons of let 'm:'(nat) in 'a * ('(m),'a) listl : ('(m+1),'a) listl

该(m+1)是在类型级别上完成的。非常整洁。

但是，最新版本来自2007年(OCaml 3.08)。有没有人知道为什么这个项目被取消了，或者今天是否有类似的OCaml？

Answer 1

在计算机科学研究期间编写的大多数软件都是一个原型，它的开发不会比提出本文的科学观点所需的开发更深入，从而验证您的方法。一些例外最终被维护了很长一段时间，过着复杂的生活，成为人们依赖的东西(OCaml就是这样的一个例子)，但这既是好事也是坏事。

我从来没有想过Concoqtion是为了立即采用，而是作为一个概念的证明，你可以集成编程和证明“现在！”。从“采用”的角度来看，MetaOcaml已经是OCaml上的一个很少使用的补丁，在这个组合中添加Coq (它既不是轻量级的，也不是为嵌入而设计的)给了你一个相当脆弱的系统的合理承诺，这个系统将很难长期维护。

我不会说Concoqtion是“废弃的”，而不是给我们上了一课，但并不意味着要真正使用它。研究人员一直在这一领域工作，许多系统都可以被描述为这项工作的后代(或者至少重用了一些想法)，例如VeriML。

当然，我是以局外人的身份这么说的。很难猜测作者的意图是什么。此外，在研究界，与原型/产品经常有一种模棱两可的关系:你通常认为没有人会采用你的实验软件，但也许，也许有些人确实会有一点希望。作者本身通常对于他们的开发是打算将其作为一个一次性原型，还是积极地期望用户参与进来(你通常不会在你的论文或网页上写下“我们故意偷工减料，破解丑陋的狗屎，使它在论文的几个例子上几乎没有足够的效果”)。有些人设计了非常可靠的软件，但是从来没有被采用(向Alice ML致敬)，有些人开发了薄薄的原型，供其他人使用(没有例子)，你永远不会知道。