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.
To formally verify Rust programs, we are building coq-of-rust, a translator from Rust聽馃 code to the proof system Coq聽馃悡. We generate Coq code that is as similar as possible to the original Rust code, so that the user can easily understand the generated code and write proofs about it. In this blog post, we explain how we are representing side effects in Coq.
With our project coq-of-rust we aim to translate high-level Rust code to similar-looking Coq code, to formally verify Rust programs. One of the important constructs in the Rust language is the method syntax. In this post, we present our technique to translate Rust methods using type-classes in Coq.
We are diversifying ourselves to apply formal verification on 3锔忊儯 new languages with Solidity, Rust, and TypeScript. In this article we describe our approach. For these three languages, we translate the code to the proof system 馃悡聽Coq. We generate the cleanest聽馃Ъ possible output to simplify the formal verification聽馃搻 effort that comes after.
Formal verification is a way to ensure that a program follows its specification in聽馃挴% of cases thanks to the use of mathematical methods. It removes far more bugs and security issues than testing, and is necessary to deliver software of the highest quality聽馃拵.