12 posts tagged with "translation"

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.

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)