search

rust-lang / rfcs

RFCs for changes to Rust
https://rust-lang.github.io/rfcs/
Apache License 2.0
5.9k stars 1.56k forks source link

Program extraction from Coq #667

Open steveklabnik opened 9 years ago

steveklabnik commented 9 years ago

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.

kmcallister commented 9 years ago

@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 commented 9 years ago

cc me

ticki commented 8 years ago

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

burdges commented 8 years ago

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

Ericson2314 commented 7 years ago

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

ticki commented 7 years ago

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

jonhoo commented 6 years ago

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.