Concoqtion (Coq + MetaOCaml) - perché abbandonato?

Question

Prima di mandare bug alle persone sulla mailing list di OCaml, ho pensato che avrei potuto postare la mia domanda qui. Ho appena scoperto questo beauty (link al sito web di Concoqtion). Concoqtion è un'estensione di MetaOCaml che consente tipi indicizzati (e forse molto di più). Con esso, è facile creare elenchi quale tipo includono anche la lunghezza della lista:

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

Questo (m+1) viene fatto a livello tipo. Molto pulito.

Tuttavia, l'ultima versione è del 2007 (OCaml 3.08). Qualcuno ha idea del perché questo progetto è stato cancellato, o se c'è qualcosa di simile per OCaml oggi?

Answer 1

La maggior parte del software scritto durante la ricerca sull'informatica è un prototipo che non si sviluppa molto più di quanto è necessario per rendere il punto scientifico dell'articolo, convalidando il tuo approccio. Alcune eccezioni finiscono per essere mantenute per lungo tempo e vivono la vita complessa di diventare qualcosa di persone dipendono da (OCaml è uno di questi esempi), ma è sia una benedizione che una maledizione.

Non ho mai pensato che Concoqtion fosse pensato per l'adozione immediata, piuttosto come una dimostrazione del concetto che è possibile integrare la programmazione e dimostrare "ora!". Dal punto di vista dell'adozione, MetaOcaml era già una patch raramente utilizzata su OCaml, aggiungendo Coq (che non è leggero né progettato per l'incorporamento) nel mix ti dà ragionevoli promesse di un sistema piuttosto fragile che sarà l'inferno da mantenere per molto tempo.

Non direi che Concoqtion è stato "abbandonato", piuttosto che ci ha insegnato una lezione, ma non è stato pensato per essere effettivamente utilizzato. I ricercatori hanno continuato a lavorare in quell'area e molti sistemi potrebbero essere descritti come discendenti (o almeno riutilizzando alcune idee da) questo lavoro, ad esempio VeriML.

Naturalmente, lo dico come un estraneo. È difficile indovinare quale fosse l'intento degli autori. Inoltre, c'è spesso un rapporto ambiguo con prototipi/prodotti nei circoli di ricerca: in genere si assume che nessuno adotterà il proprio software sperimentale, ma forse, forse c'è una piccola speranza che alcune persone effettivamente fanno. Gli autori stessi sono in genere piuttosto ambivalenti sul fatto che intendessero il loro sviluppo come prototipo di lancio o aspettano attivamente che gli utenti vengano coinvolti (in genere non scrivono "noi tagliamo intenzionalmente gli angoli e fanno una brutta merda per farlo funzionare a malapena sul alcuni esempi del documento "nella tua carta o nella tua pagina web). Alcune persone progettano un software davvero solido che tuttavia non viene mai adottato (punta di cappello su Alice ML), alcune persone sviluppano prototipi scagliosi che vengono utilizzati da altre persone (nessun esempio), non si sa mai.