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)