pirapira/coq2rust
View on GitHub ↗ ★ 226 OCaml
Coq to Rust program extraction. The whole tree is on the original Coq code base.
4 mentions on Hacker News by 4 people: 1 story, 3 comments · first 2016-07-22 · latest 2019-04-14
20082026
-
…Rust program extraction for Coq, although I wouldn't be surprised if it's not as mature as C yet: https://github.com/pirapira/coq2rust In other areas, Rust already has an advantage; compare Cargo with the Babylonian chaos of C++ build…
comment by the_why_of_y · 2019-04-14 · in Moving to a provenance-aware memory object model for C: proposal for C2x -
Most of the action happens in this file: https://github.com/pirapira/coq2rust/blob/rust/plugins/extra... I have considered attempting to write a few code extraction plugins for Coq, but I took a long look at the extraction plugin for Scala…
comment by harveywi · 2016-07-28 · in Coq to Rust Program Extraction -
▲ 99
Coq to Rust Program Extractionstory by kushti · 2016-07-28 · 18 comments
-
…C) code? Haven't tried it but this claims to be able to extract Rust programs from Coq proofs: https://github.com/pirapira/coq2rust
comment by seanwilson · 2016-07-22 · in A Formal Verification of Rust's Binary Search Implementation