Haskell Tools from the Programatica Project

2003 Haskell Workshop Demo Abstract by Thomas Hallgren

1. Introduction

One of the goals of the Programatica Project is to develop tool support for high-assurance programming in Haskell. We have extended Haskell with syntax for property assertions, and envision the use of various techniques to provide evidence for the validity of assertions. We expect our tools to assist the programmer with evidence management, using certificates to record evidence, and to provide whatever translation of Haskell code needed to enable the use of theorem provers and other tools that can serve as sources of evidence.

The Programatica Tools, while still work in progress, can manipulate Haskell programs in various ways and have some support for evidence management. In Section 2, we describe a selection of the functionality provided by the tools, starting with functionality that might be of interest to Haskell programmers in general, and ending with functionality more directly aimed at supporting the goals of the Programatica Project. Section 3 contains some notes on the implementation.