19 Feb
2009
19 Feb
'09
9:15 a.m.
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