We explained how we started updating our translation tool coq-of-rust in our previous blog post, to support more of the Rust language. Our goal is to provide formal verification for the Rust聽馃 language, relying on the proof system Coq聽馃悡. We will see in this post how we continue implementing changes in聽coq-of-rust
to:
- remove the types from the translation,
- be independent of the ordering of the definitions.