I am trying to create some project in rust and Coq, Currently I am literally rewriting code manually, is there a way to automat the process of generating code from coq to rust ?
I see there is an old project from 2014 that claims to do that: https://github.com/pirapira/coq2rust but the project is ocaml an I am worried it is dead (and I don't know ocaml so if it is not working, I won't be able to fix it quickly)
maybe look at https://arxiv.org/abs/2108.02995
I don't know how well it works
https://rust-formal-methods.github.io/tools.html has some Coq-related links
More information on rust extraction using ConCert is here: https://github.com/AU-COBRA/ConCert
@walker is there anything you need from rust extraction that's not already in concert?
@Bas Spitters I only noticed this message right now so sorry for late reply:
Actually yes the project works only for old Coq, I tried porting to modern coq and it was not trivial. That will be something that I will heavily rely on for my PhD and I am worried that CompCert is just academic project that will die once funding stop.
I actually also believe that it will be hard to write Trustworthy extraction plugin for rust since there are some trickery with MiniML so unfortunately I might move to something with already existing FFI like lean4.
Still I am happy that I learned coq first. It was instructive.
if you're looking at formal verification projects in academia, CompCert is probably one of the most likely to live on for a while. Besides basic connections to Inria which has sustained funding through French government, it also has the commercial side: https://www.absint.com/compcert/index.htm
Actually yes the project works only for old Coq, I tried porting to modern coq and it was not trivial.
getting help for that may work better than getting help for a new extraction backend
There might be some confusion between ConCert and CompCert?
ah, ConCert is a more academic framework
yes, the preferred approach around here when we need some code to work with recent Coq is to work with code authors
thanks to Coq's code compatibility policy, it's usually not a big deal to port between versions using the changelog
we're talking about plugins not .v code, the changelog is basically useless for porting plugins
but is ConCert really much of a plugin? Last time I checked, it was mostly Coq code, and then it uses MetaCoq
according to cloc
, ConCert repo has no OCaml code at all
you can be right, I could have talked to the authors but I took the easy way out and decided to just use lean
also I wouldn't compare compcert to concert, I would consider compcert an anomaly, it is one of the very few academic project that lived on.
Didn't Ocaml live on? Didn't Coq? Also, you mention your PhD, isn't it going to be an academic project too?
I'd say Bas has a pretty good record of keeping Coq projects alive at this point... CoRN is around 20 years old
I get your point, maybe I am over paranoid, I never knew the author, I would like nothing more than looking back and realizing that I was wrong.
In any was it was also fun learning Ocaml, I had to learn it in my failing attempt to write the plugin.
also was cool exploring Coq's source code.
Also, you mention your PhD, isn't it going to be an academic?
Good question, So It is industrial PhD and while it is understandable that papers are cool an essential for the Degree, the industrial partner (also the ones who pay for everything) are solely interested in Code that works reliably, an it will be nightmare if anything I use turned into fix it yourself kind of projects.
I worked in some projects like that in the past, But Ocaml and Coq are (same for compcert and any project with commits 5+ years after it it was first published). And those project lived for like 20+ years not just 5 so yes they are reliable. That why I trust that Coq and Ocaml are not going anywhere soon.
If you are worried about durability, then using Lean4 looks like a strange choice. Lean4 is still alpha (or beta) software and its author has a history of breaking user's code without looking back. On the contrary, the Coq ecosystem has a history of deeply caring about compatibility and upgrading.
mmm, I will have to think about it. my problem is not with coq, it is with coq's support for Rust extraction.
see also https://github.com/leanprover/lean4/blob/master/doc/faq.md#should-i-use-lean
Could you explain why you think Lean is the easy way out?
Imo the json extraction module is the option giving you the most freedom. I could even imagine Lean or agda producing the same kind of output. Then you use what you want. Of course, not using something already existing, does not seem the quickest option. In particular, software rarely gets written well the first time, and the prototype better be written quickly (not from scratch) since you are going to toss it anyway.
walker said:
mmm, I will have to think about it. my problem is not with coq, it is with coq's support for Rust extraction.
This is not necessarily the most recommended option (for various reasons that others can ellaborate), but if you were to write a Rust extraction plugin in OCaml, then you could benefit from upgrades from one version to the next by adding it into Coq's CI. See https://github.com/coq/coq/blob/master/CONTRIBUTING.md#support-for-plugin-and-library-authors.
The comments about plugins quickly bitrotting relate to plugins that are not in Coq's CI (for instance, because their authors have created them for a version of Coq that was already not master
and never upgraded them to master
which is necessary to get into Coq's CI).
I admit, lean is more cumbersome than I thought, I am back to coq. The problem with writing my own extraction plugin is that it was best-effort, there were many corrner cases with polymorphism that were were not handled.
so the solution I am attempting next is just extracting to OCAML and see if I can use OCaml ffi interface in rust
I'd recommend using the FFI approach given here (go via C FFI): https://github.com/xavierleroy/camljava
@walker Aside, since you're doing a PhD, I'd recommend using your real name and affiliation. But that's up to you.
The concert's extraction to rust is build on metacoq, a central and well-supported part of Coq.
If you're serious about contributing to it, we could discuss moving some parts to a more central place.
In fact, we're already working with the metacoq team on tighter integration. They are working on certified extraction to ocaml.
walker has marked this topic as resolved.
Hi @walker , thank you for your interest in our project! I'm currently porting ConCert to Coq 8.14, the non-trivial bit comes from MetaCoq that has changed quite a bit. Rust extraction is ported already, I'll ping you once I get something you can build. Personally, I would be glad if someone could pick up Rust extraction and improve it. Also, as @Bas Spitters mentioned, we would like to move some general parts to MetaCoq, this would help to make maintenance simpler in the future.
@walker ConCert is now compatible with Coq 8.15 https://github.com/AU-COBRA/ConCert
There is also branches for Coq 8.14 https://github.com/AU-COBRA/ConCert/tree/coq-8.14
and Coq 8.11 https://github.com/AU-COBRA/ConCert/tree/coq-8.11
Do you mean "now" rather than "not"?
Ah, yes, sorry, you're right @Meven Lennon-Bertrand :) "ConCert is now compatible with Coq 8.15"
(I've edited the comment)
That is perfect!
Last updated: Oct 01 2023 at 19:01 UTC