types - Concoqtion (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

在计算机科学研究期间编写的大多数软件都是一个原型(prototype)，没有比提出文章的科学观点所需的更进一步，验证你的方法。有些异常(exception)最终会维持很长时间，过着复杂的生活，成为人们依赖的东西(OCaml 就是这样一个例子)，但这既是福也是祸。

我从不认为 Concoqtion 意味着立即采用，而是作为概念证明，您可以集成编程和“现在!”证明。从“采用”的角度来看，MetaOcaml 已经是 OCaml 之上的一个很少使用的补丁，在混合中添加 Coq(不是轻量级的，也不是为嵌入而设计的)给你一个相当脆弱的系统的合理 promise ，它将是 hell 维持了很长时间。

我不会说 Concoqtion 被“抛弃”，而不是它给我们上了一课，但并不打算实际使用。研究人员一直在该领域工作，许多系统可以被描述为这项工作的后代(或至少重用了一些想法)，例如 VeriML .

当然，我是作为一个局外人这么说的。很难猜出作者的意图是什么。此外，在研究圈中，原型(prototype)/产品常常存在一种模棱两可的关系:您通常假设没有人会采用您的实验软件，但也许，也许有些人实际这样做的希望很小。对于他们是否打算将他们的开发作为一次性原型(prototype)，或者积极期望用户参与其中，作者自己通常相当矛盾(你通常不会写“我们故意偷工减料并砍掉丑陋的狗屎，使其在论文的几个例子”在你的论文或你的网页上)。有些人设计了真正可靠的软件，但从未被采用(向 Alice ML 致敬)，有些人开发了被其他人使用的片状原型(prototype)(没有示例)，你永远不知道。