Concoqtion (Coq + MetaOCaml) - why refused?

Question

Before listening to people on the OCaml mailing list, I thought I could post my question here. I just discovered this beauty (link to Concoqtion website). Concoqtion is a MetaOCaml extension that allows you to index types (and possibly much more). With its help it is easy to create lists, the type of which also includes 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 

This (m+1) is done at the type level. Very neat.

However, the latest version is from 2007 (OCaml 3.08). Does anyone have an idea why this project was canceled, or if today there is something similar to OCaml?

Answer 1

Most of the software written during research in computer science is a prototype that does not develop much further than what is needed in order to make a scientific point of the article, confirming your approach. Some exceptions ultimately persist for a long time and live in a complex life that people depend on (OCaml is one such example), but this is both a blessing and a curse.

I never thought Concoqtion was intended for immediate adoption, but rather as a proof of concept that you can integrate programming and prove "now!". In terms of “adoption”, MetaOcaml was already a rarely used patch attached to OCaml, adding that Coq (which is not lightweight and not intended for embedding) in the mix gives a reasonable promises a rather fragile system that will be hell to maintain for a long time.

I would not say that Concoqtion was “abandoned”, and not taught us a lesson, but was not intended for actual use. Researchers continued to work in this area, and many systems could be described as descendants (or at least reuse some ideas) of this work, for example VeriML .

Of course, I say this as an outsider. It is hard to guess what the intentions of the authors are. Moreover, there is often an ambiguous relationship with prototypes / product in research circles: you usually assume that no one will accept your experimental software, but maybe there is little hope that some people really do. The authors themselves, as a rule, are rather ambiguous as to whether they planned their development as a prototype of the outlier or actively expect users to be involved (you usually won’t write “we deliberately cut corners and cracked ugly shit so that it barely worked on a few examples of paper "in your article or on your web page). Some people develop really reliable software, which, however, is never accepted (a tip for Alice ML ), some people develop flaky prototypes that are used by other people (no example), you never know.