Why Agda

Agda adds a new dimension of formality to programming. It allows formal specifications to be written that can be both proven and executed. It integrates directly with Haskell - Agda specifications can be extracted into Haskell modules that can be linked with existing and new Haskell code. This increases confidence that the source code precisely and correctly meets its functional requirements. Why program when you can generate?