Program extraction from Coq

[kmcallister]

There are a number of interesting, proven-correct data structure implementations in Coq, e.g. https://www.lri.fr/~filliatr/puf/. Coq programs can be extracted as Haskell, OCaml, or Scheme. Because of pattern matching and other functional features, Rust is a more attractive target for extraction than most other systems languages.

Another application is to write the unsafe part of a Rust program in Coq, with a safety proof. You can decide what safety properties to provide, within a model that can vary from the Rust machine model. This is a lot more flexible (and a lot more work!) than the all-or-nothing nature of unsafe.

Because all three existing target languages use garbage collection, the extracted Rust code may need to rely heavily on reference counting. However this is perfectly reasonable when extracting functional persistent data structures, which inevitably have non-unique ownership.

It would also be neat to embed affine types into Coq although I'm not sure what has been done or can be done here.

[kmcallister]

The existing extraction plugins are about 200 - 700 lines of OCaml each.

[JasonGross]

Regarding embedding affine types in Coq, you could do a deep embedding of the lambda calculus and declare the extraction of various constants, but this would probably be painful to use. If affine types are a deal-breaker, you might want to look into Idris, which has uniqueness types. Or you can develop affine types for Coq and extend Coq's typechecker, which would be an even bigger project than this issue suggests, but would be pretty awesome.

[jroesch]

cc me, I would be interested if anyone pursues this.

[pirapira]

I started writing a Coq-to-Rust extraction. It relies on lots of boxes. I am adding a new construct every week or two. https://github.com/pirapira/coq2rust

[steveklabnik]

I'm pulling a massive triage effort to get us ready for 1.0. As part of this, I'm moving stuff that's wishlist-like to the RFCs repo, as that's where major new things should get discussed/prioritized.

This issue has been moved to the RFCs repo: rust-lang/rfcs#667