Skip to main content

5 posts tagged with "translation"

View All Tags

11 min read

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:

  1. remove the types from the translation,
  2. be independent of the ordering of the definitions.

10 min read

In our previous blog post, we stated our plan to improve our translation of Rust聽馃 to Coq聽馃悡 with coq-of-rust. We also provided a new definition for our Rust monad in Coq, and the definition of a unified type to represent any Rust values. We will now see how we modify the Rust implementation of聽coq-of-rust to make the generated code use these new definitions.

With this new translation strategy, to support more Rust code, we want:

  1. to remove the types from the translation,
  2. to avoid the need to order the definitions in the generated Coq code.

13 min read

Our tool coq-of-rust is translating Rust聽馃 programs to the proof system Coq聽馃悡 to do formal verification on Rust programs. Even if we are able to verify realistic code, such as an ERC-20 smart contract, coq-of-rust still has some limitations:

  • fragile trait handling
  • difficulties in ordering the definitions, in their order of dependencies as required by Coq

We will present how we plan to improve our tool to address these limitations.

13 min read

In this blog post, we present our development steps to build a tool to translate Go programs to the proof system Coq.

The goal is to formally verify Go programs to make them totally bug-free. It is actually possible to make a program totally bug-free, as formal verification can cover all execution cases and kinds of properties thanks to the use of mathematical methods. This corresponds to the highest level of the Evaluation Assurance Levels used for critical applications, such as the space industry.

All the code of our work is available on GitHub at github.com/formal-land/coq-of-go-experiment.

5 min read

We present an experiment coq-of-hs that we have made on the translation of Haskell programs to the proof system Coq聽馃悡. The goal is to formally verify Haskell programs to make them totally bug-free.

Indeed, even with the use of a strict type system, there can still be bugs for properties that cannot be expressed with types. An example of such a property is the backward compatibility of an API endpoint for the new release of a web service when there has been code refactoring. Only formal verification can cover all execution cases and kinds of properties.

The code of the tool is at: github.com/formal-land/coq-of-hs-experiment (AGPL license)