Skip to main content

One post tagged with "coq-of-hs"

View All Tags

ยท 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: (AGPL license)