Unfortunately the "proofs" in dependently typed languages are extremely long and tedious to write. Some kind of compiler proofing tool could ease the pain, but I do not think it has low enough complexity for a GSoC project. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net | 877-376-2724 x 101 On Feb 19, 2009, at 1:37 AM, Wolfgang Jeltsch wrote:
Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain:
Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support.
Wouldn’t it be better to achieve the goals you describe with a dependently typed programming language?
Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe