Skip to main content

One post tagged with "HIR"

View All Tags

ยท 6 min read

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.