Concoqtion (Coq + MetaOCaml) - why abandoned?

Question

Before bugging people on the OCaml mailing list, I thought I might post my question here. I just discovered this beauty (link to Concoqtion website). Concoqtion is an extension of MetaOCaml which allows indexed types (and perhaps a lot more). With it, it's easy to create lists which type also include the length of the list:

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

That (m+1) is done on the type level. Very neat.

However, the last version is from 2007 (OCaml 3.08). Have anyone any idea why this project got cancelled, or if there is something similiar for OCaml today?

Answer 1

Most of the software written during computer science research is a prototype that is not developed much further than what is needed to make the scientific point of the article, validating your approach. Some exceptions end up being maintained for a long time and living the complex life of becoming something people depend on (OCaml is one such example), but that is both a blessing and a curse.

I never thought Concoqtion was meant for immediate adoption, rather as a proof of concept that you can integrate programming and proving "now!". From an 'adoption' point of view, MetaOcaml was already a rarely-used patch tacked on top of OCaml, adding Coq (that is not lightweight nor designed for embedding) in the mix gives you reasonable promises of an rather brittle system that will be hell to maintain over a long time.

I wouldn't say that Concoqtion was "abandoned", rather than it taught us a lesson, but was not meant to actually be used. Researchers kept working in that area, and lots of systems could be described as descendants (or at least reusing some ideas from) this work, for example VeriML.

Of course, I say that as an outsider. It's hard to guess what the intent of the authors was. Moreover, there is often an ambiguous relation with prototypes/product in research circles: you generally assume that nobody will adopt your experimental software, but maybe, maybe there is a small hope that some people actually do. The authors themselves are generally rather ambivalent on whether they intended their development as a throw-away prototype, or actively expect users to get involved (you will generally not write "we intentionally cut corners and hacked ugly shit to make it barely work enough on the few examples of the paper" in your paper or on your webpage). Some people design really solid software that however never gets adopted (hat tip to Alice ML), some people develop flaky prototypes that get used by other people (no example), you never know.