Am Donnerstag, 19. Februar 2009 14:50 schrieb John A. De Goes: > 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.
I was not saying that I want such a thing done as a GSoC project. I just wanted to say that if one wants a programming language with an integrated proof language, it might be better to put work into Agda or Epigram instead of extending Haskell. Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
