Combining dependent types with dynamic checks and monitoring

Combining dependent types with dynamic checks and monitoring
Master Project of Jakob Naucke

Problem statement

Dependent types are a powerful tool for ensuring the correctness of our programs. However, proving correctness of our programs is a daunting task, especially in the initial phases of a project when a full specification is not yet known. Hence we should provide the programmer with a gradual path to higher degrees of verification: from a few isolated unit tests to property-based tests to dynamic monitoring of the properties to full static verification.

Project description

The goal of this project is to extend the Agda2Hs tool with additional capabilities for checking program correctness, in particular property-based testing and run-time monitoring of properties that are stated in the Agda code but do not yet have a (complete) proof. An important challenge will be to figure out which Agda types can be converted to run-time checks, and how this conversion can be implemented automatically. In addition, in case of a run-time violation of a property we would like to give an indication to the programmer of where exactly the problem originated. This could for example be done by using a blame calculus, as introduced by Philip Wadler and Robby Findler in their 2007 paper Well-typed Programs Can’t Be Blamed.