Concoqtion (Coq + MetaOCaml) - warum aufgegeben?

Question

Bevor ich Leute auf der OCaml-Mailingliste abgehört habe, dachte ich, ich könnte meine Frage hier posten. Ich habe gerade diese beauty entdeckt (Link zur Concoqtion Website). Concoqtion ist eine Erweiterung von MetaOCaml, die indizierte Typen erlaubt (und vielleicht noch viel mehr). Mit ihm ist es einfach, Listen zu erstellen, welche Art auch die Länge der Liste ist:

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

Die (m+1) ist auf dem Typenebene. Sehr gepflegt.

Die letzte Version ist jedoch von 2007 (OCaml 3.08). Hat jemand eine Idee, warum dieses Projekt abgesagt wurde, oder ob es heute etwas Ähnliches für OCaml gibt?

Answer 1

Die meiste Software, die während der Informatikforschung geschrieben wird, ist ein Prototyp, der nicht viel weiter entwickelt wird als das, was benötigt wird, um den wissenschaftlichen Punkt des Artikels zu machen und Ihren Ansatz zu validieren. Einige Ausnahmen werden für eine lange Zeit aufrechterhalten und leben das komplexe Leben des Werdens Menschen abhängen auf (OCaml ist ein solches Beispiel), aber das ist sowohl ein Segen und ein Fluch.

Ich hätte nie gedacht, Concoqtion war für die sofortige Annahme gedacht, eher als ein Beweis des Konzepts, dass Sie Programmierung und Prüfung "jetzt!" Integrieren können. Von einer "Adoption" Sicht war MetaOcaml bereits ein selten verwendetes Patch auf OCaml angeheftet, Hinzufügen von Coq (das ist nicht leicht oder für die Einbettung) in der Mischung gibt Ihnen vernünftige Versprechungen von einem eher spröde System, das sein wird die Hölle für eine lange Zeit aufrecht zu erhalten.

Ich würde nicht sagen, dass Concoqtion wurde "aufgegeben", anstatt es uns eine Lektion gelehrt, sollte aber nicht wirklich verwendet werden. Die Forscher arbeiteten weiter in diesem Bereich, und viele Systeme konnten als Nachfahren beschrieben werden (oder zumindest einige Ideen aus dieser Arbeit wiederverwenden), zum Beispiel VeriML.

Natürlich sage ich das als Außenseiter. Es ist schwer zu erraten, was die Absicht der Autoren war. Darüber hinaus gibt es in Forscherkreisen oft eine mehrdeutige Beziehung zu Prototypen/Produkten: Man geht davon aus, dass niemand Ihre experimentelle Software übernehmen wird, aber vielleicht gibt es eine kleine Hoffnung, die manche Leute tatsächlich haben. Die Autoren selbst sind im Allgemeinen eher ambivalent, ob sie ihre Entwicklung als Wegwerfprototyp beabsichtigen oder aktiv erwarten, dass sich Nutzer einbringen (Sie werden generell nicht schreiben "wir schneiden absichtlich ab und hacken hässliche Scheiße, damit es auf der einige Beispiele des Papiers "in Ihrem Papier oder auf Ihrer Webseite". Einige Leute entwerfen wirklich solide Software, die jedoch nie angenommen wird (Hut Tipp zu Alice ML), einige Leute entwickeln flockige Prototypen, die von anderen Leuten benutzt werden (kein Beispiel), Sie können nie wissen.