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

コンピュータサイエンスの研究で書かれたソフトウェアのほとんどは、記事の科学的なポイントを作るために必要なものよりもはるかに発展しておらず、あなたのアプローチを検証するプロトタイプです。いくつかの例外は長年にわたって維持され、何かになることの複雑な生活を続けるはに依存しますが（OCamlはそうした例の1つですが）、それは祝福と呪いの両方です。

Concoqtionは、プログラミングを統合して「今すぐ」ということを証明できる概念の証明ではなく、すぐに採用されるとは決して考えませんでした。 「採用」の観点から見ると、MetaOcamlはすでにOCamlの上に貼られためったに使われていないパッチであり、Coq（軽量でも埋め込み用にも設計されていない）を追加することで、脆弱なシステムの合理的な約束が得られます地獄は長い間維持する。

私はConcoqtionがレッスンを教えてくれるのではなく、 "放棄"されているとは言いませんが、実際に使用するつもりはありませんでした。研究者はその分野で作業を続けており、多くのシステムはこの作業の子孫として記述することができます（または、少なくともなど）。

もちろん、私はアウトサイダーとして言います。著者の意図が何であるかを推測するのは難しいです。また、研究サークルのプロトタイプ/製品とのあいまいな関係があることがよくあります。通常、誰もあなたの実験的なソフトウェアを採用しないと想定していますが、実際には小さな希望があるかもしれません。著者自身は、一般的に、開発を意図したプロトタイプとして意図しているのか、ユーザーが積極的に参加することを期待しているのかについて、あまり意識していません（「意図的にコーナーをカットし、紙の中のいくつかの例、またはあなたのウェブページ上の例）。しかし、決して採用されない堅実なソフトウェアを設計する人もいる（帽子の先端はAlice ML）、他の人々（例はありません）によって使用される薄れたプロトタイプを開発する人もいます。