Concoqtion (Coq + MetaOCaml) - tại sao bị bỏ rơi?

Question

Trước khi làm phiền mọi người trong danh sách gửi thư của OCaml, tôi nghĩ tôi có thể đăng câu hỏi của mình ở đây. Tôi vừa phát hiện ra điều này beauty (liên kết đến trang web Concoqtion). Concoqtion là một phần mở rộng của MetaOCaml cho phép các loại được lập chỉ mục (và có lẽ nhiều hơn nữa). Với nó, thật dễ dàng để tạo danh sách loại cũng bao gồm độ dài của danh sách:

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

Điều đó (m+1) được thực hiện ở cấp độ loại. Rât gọn gang.

Tuy nhiên, phiên bản cuối cùng là từ năm 2007 (OCaml 3.08). Có bất cứ ai có ý tưởng tại sao dự án này đã bị hủy bỏ, hoặc nếu có một cái gì đó tương tự cho OCaml ngày hôm nay?

Answer 1

Hầu hết phần mềm được viết trong nghiên cứu khoa học máy tính là một mẫu thử nghiệm không được phát triển nhiều hơn những gì cần thiết để làm cho điểm khoa học của bài viết, xác thực cách tiếp cận của bạn. Một số trường hợp ngoại lệ kết thúc được duy trì trong một thời gian dài và sống cuộc sống phức tạp trở thành một cái gì đó mọi người phụ thuộc trên (OCaml là một ví dụ), nhưng đó là cả một phước lành và một lời nguyền.

Tôi chưa bao giờ nghĩ Concoqtion có ý nghĩa cho việc áp dụng ngay lập tức, thay vì bằng chứng về khái niệm mà bạn có thể tích hợp lập trình và chứng minh "ngay bây giờ!". MetaOcaml đã trở thành một bản vá hiếm khi được sử dụng ở trên cùng của OCaml, thêm Coq (không nhẹ và cũng không được thiết kế để nhúng) trong hỗn hợp mang lại cho bạn lời hứa hợp lý về một hệ thống khá giòn địa ngục để duy trì trong một thời gian dài.

Tôi sẽ không nói rằng Concoqtion bị "bỏ rơi", thay vì nó dạy chúng ta một bài học, nhưng không có nghĩa là thực sự được sử dụng. Các nhà nghiên cứu tiếp tục làm việc trong khu vực đó và nhiều hệ thống có thể được mô tả như là con cháu (hoặc ít nhất là sử dụng lại một số ý tưởng từ) tác phẩm này, ví dụ: VeriML.

Tất nhiên, tôi nói đó là người ngoài. Thật khó để đoán ý định của các tác giả là gì. Hơn nữa, thường có một mối quan hệ mơ hồ với nguyên mẫu/sản phẩm trong các vòng nghiên cứu: bạn thường giả định rằng không ai sẽ áp dụng phần mềm thử nghiệm của bạn, nhưng có lẽ, có thể có một hy vọng nhỏ mà một số người thực sự làm. Bản thân các tác giả nói chung là khá mâu thuẫn về việc họ dự định phát triển của họ như là một nguyên mẫu ném đi hay chủ động mong đợi người dùng tham gia (nói chung là bạn không viết "chúng tôi cố ý cắt góc và tấn công xấu xí để làm cho nó không hoạt động đủ trên vài ví dụ về bài báo "trong bài viết của bạn hoặc trên trang web của bạn). Một số người thiết kế phần mềm thực sự vững chắc tuy nhiên không bao giờ được thông qua (mũ tip để Alice ML), một số người phát triển nguyên mẫu flaky mà được sử dụng bởi những người khác (không có ví dụ), bạn không bao giờ biết.