Talk:Proof: Difference between revisions
→Haskell: compile == proof?
(→Draft status: re) |
(→Haskell: compile == proof?) |
||
Line 151:
Looks like GHC can typecheck the same expression as in the Omega/Agda version. Сan not guarantee the totality, however. — [[User:Ht|Ht]] 02:52, 12 May 2012 (UTC)
Does it satisfy the task? Hard to say due to existing inconsistencies in the task description. The description starts out saying it only makes sense for dependently typed languages and proof assistants. It later wants to allow Haskell for implementing System-F. Is type checking enough, and if so, must it be run time or can it be compile time? My understanding is that dependent typing, by definition, is done at run time and that Haskell does the type checking at compile time. Does a clean compile constitute a proof?
| |||