[bitc-dev] Programming with theorem proving: Concoqtion

[Sandro Magi]

They recently released the Concoqtion, which is MetaOCaml integrated
with the Coq theorem prover:

"Concoqtion is an extension to MetaOCaml with indexed types. [...] Only
a small number of extensions to the term and type language are needed to
give the user full access to the powerful Coq proof checker at the level
of types. [...] Because Coq is one of the most expressive checkers
available, any fact that can be proved in Coq can be used to give more
refined types to programs. Because Coq propositions can be viewed as
types, Concoqtion provides a natural way to incorporate formal
verification techniques into programming practice."

http://www.metaocaml.org/concoqtion/