Concoqtion (Coq + MetaOCaml) - почему отказались?

Question

Перед тем, как записывать людей в список рассылки OCaml, я подумал, что могу опубликовать свой вопрос здесь. Я только что обнаружил эту красоту (ссылка на сайт 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.

Конечно, я говорю это как посторонний. Трудно догадаться, что было задумано авторами. Более того, в исследовательских кругах часто возникает неоднозначная связь с прототипами / продуктами: вы обычно предполагаете, что никто не примет ваше экспериментальное программное обеспечение, но, может быть, есть небольшая надежда, что некоторые на самом деле это делают. Сами авторы, как правило, довольно двусмысленны в отношении того, планировали ли они свою разработку в качестве одноразового прототипа, или активно ожидают, что пользователи будут участвовать (вы, как правило, не будете писать "мы преднамеренно сократили углы и взломали отвратительное дерьмо, чтобы заставить его едва работать на несколько примеров из бумаги "в вашей газете или на вашей веб-странице). Некоторые люди разрабатывают действительно надежное программное обеспечение, которое, тем не менее, никогда не будет принято (как на ладони Алисе МЛ), некоторые люди разрабатывают непрочные прототипы, которые используются другими людьми (без примера), вы никогда не знаете.