Program extraction from Coq

Issue by kmcallister
Friday Oct 31, 2014 at 20:30 GMT

For earlier discussion, see https://github.com/rust-lang/rust/issues/18496

This issue was labelled with: A-an-interesting-project, E-hard in the Rust repository

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.

Start with the earlier discussion in rust-lang/rust#18496 and the Coq Reference Manual section on program extraction. Determine the intended extraction target, Rust ownership and memory-management model, and whether affine types are in scope. Done would require a settled design and implementation plan for extracting Coq programs to Rust.