Program extraction from Coq

[steveklabnik]

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

For earlier discussion, see rust-lang/rust#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.

[kmcallister]

@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

[jroesch]

cc me

[ticki]

This is really interesting. Coq is very powerful. I wonder how well Coq would intergrate with Rust.

[burdges]

I'm just curious : How are closures being mapped to Rust's closures?

[Ericson2314]

I wonder whether GC will help with this (e.g. cycles from codata)

[ticki]

http://ticki.github.io/blog/a-hoare-logic-for-rust/

[jonhoo]

Another way to get around the reference counting issue might be to use an arena allocator. This would work particularly well for large cyclic datastructures that are collapsed all at once.