25 Apr
2007
25 Apr
'07
6:38 a.m.
Tim Newsham
- 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