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
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
