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 - один из таких примеров), но это и благословение, и проклятие.

Я никогда не думал, что Concoqtion предназначено для немедленного принятия, а как доказательство концепции, что вы можете интегрировать программирование и доказывать «сейчас!». С точки зрения «принятия» MetaOcaml уже был редко используемым патчем, прикрепленным к OCaml, добавив, что Coq (который не легкий и не предназначен для встраивания) в смесь дает вам разумные обещания относительно хрупкой системы, которая будет ад для поддержания в течение длительного времени.

Я бы не сказал, что Concoqtion был «оставлен», а не учил нас уроку, но не предназначен для фактического использования. Исследователи продолжали работать в этой области, и множество систем можно было назвать потомками (или, по крайней мере, повторно использовать некоторые идеи) этой работы, например VeriML.

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