2 posts tagged with "trait"

We continued our work on coq-of-rust, a tool to formally verify Rust programs using the proof system Coq 🐓. This tool translates Rust programs to an equivalent Coq program, which can then be verified using Coq's proof assistant. It opens the door to building mathematically proven bug-free Rust programs.

We present two main improvements we made to coq-of-rust:

• Using the THIR intermediate language of Rust to have more information during the translation to Coq.
• Bundling the type-classes representing the traits of Rust to have faster type-checking in Coq.

In our project coq-of-rust we translate programs written in Rust to equivalent programs in the language of the proof system Coq 🐓, which will later allow us to formally verify them. Both Coq and Rust have many unique features, and there are many differences between them, so in the process of translation we need to treat the case of each language construction separately. In this post, we discuss how we translate the most complicated one: traits.