-
coq-of-rust
Check 100% of execution cases of Rust programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦 Formal verification
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
That's really impressive.
Automatic translation like this shifts the trust to the tool. coq-of-rust itself is written in Rust, not in Coq. The recursive nature is somewhat boggling, but I think a proof of its correctness could be done in much the same way as they do with the stdlib. To verify it, you'd use coq-of-rust to convert coq-of-rust to Coq. That translation is not trusted, because it was performed in Rust. You then undertake the process they describe in the article of proving equivalence between generated definitions and simpler hand-written definitions, which proofs are written in terms of. Once you prove that the generated Coq version of coq-of-coq translates Rust programs correctly, you use it to translate Rust coq-of-rust to Coq and compare the two. They should match. Since the current line count for coq-of-rust (specifically, lib/ [0]) is 6350 lines of Rust, this seems feasible.
It's a similar process to David A. Wheeler's “Countering Trusting Trust through Diverse Double-Compiling” (2009) [1], which circumvents Ken Thompson's Trusting Trusting attack by using a second compiler.
As an aside, it's nice to see industry funding for work like this. I'm often cynical of cryptocurrency, but its correctness constraints really push for improvements in areas I like (Rust, Coq, funding for masters students I know, etc.).
[0]: https://github.com/formal-land/coq-of-rust/tree/main/lib
You can write programs in Coq and extract them in OCaml with the `Extraction' command: https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.ht...
This is used by compcert: https://compcert.org/
wonder how much work it would be to add a rust backend to F* [https://github.com/FStarLang/FStar]