[Haskell-cafe] Reasoning [was: Tutorial on Haskell]

[Malcolm Wallace]

Tim Newsham <newsham at lava.net> wrote:

>    - What about program proofs?  Are there any systems that tie
>      directly into haskell and let you augment your haskell program
>      with a proof that can be machine checked?

Programatica.
    http://www.csee.ogi.edu/PacSoft/projects/programatica/

You can write properties in the PLogic specification language (in
comments within your program), and have them translated to the Alfa/Agda
theorem prover.  (However, I haven't seen much development activity on
the Programatica project for a couple of years now.)

Regards,
    Malcolm