gpt4 book ai didi

types - Concoqtion (Coq + MetaOCaml) - 为什么放弃?

转载 作者:行者123 更新时间:2023-12-04 10:19:05 24 4
gpt4 key购买 nike

在对 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 是否有类似的东西?

最佳答案

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

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

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

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

关于types - Concoqtion (Coq + MetaOCaml) - 为什么放弃?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/16068784/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com