Proposal to add Cocasse

[palmskog]

Move a project to coq-community

Project name: Cocasse

Initial author(s): Nicolas Tabareau and Éric Tanter

Current URL: https://github.com/tabareau/Cocasse

Kind: Coq library with extraction examples

License: unknown (need to ask authors to explicitly release under open source license)

Description: This small library demonstrates a technique for deferring proof witnesses for subset types to "computation time" by introducing some axioms. This in effect enables gradual typing when programming in Coq, with runtime checks in extracted code. The library is described in the paper Gradual certified programming in Coq.

Status: Appears unmaintained. Does not work with Coq 8.8 or 8.9.

New maintainer: looking for a volunteer

[palmskog]

While the library is seemingly unrefined, the technique appears practical and interesting and is orthogonal to other development helps such as property-based testing. It also highlights that "unsound" axioms can be helpful in practice, which a larger audience may not be aware of.

[Zimmi48]

@tabareau @etanter: Would you mind adding an open source license to this repository?