tag:blogger.com,1999:blog-5722310642266356003.post4646769715030989810..comments2024-01-07T23:21:32.676+01:00Comments on The Axis of Eval: Notes on Dependent TypesUnknownnoreply@blogger.comBlogger2125tag:blogger.com,1999:blog-5722310642266356003.post-60898017413520211782014-03-30T21:16:34.900+02:002014-03-30T21:16:34.900+02:00I think your link to e-pig.org is no longer what y...I think your link to e-pig.org is no longer what you think it is.Jorge Monasteriohttps://www.blogger.com/profile/12978901430143368088noreply@blogger.comtag:blogger.com,1999:blog-5722310642266356003.post-86390715649975394262010-10-25T19:23:47.283+02:002010-10-25T19:23:47.283+02:00Interesting. I'm currently taking a Coq course...Interesting. I'm currently taking a Coq course at my university and I was blown away by the power of dependent types.<br />Granted, I don't think that Coq is for everyday use, but writing a function and then PROVING that gives the expected output for all the inputs is amazing!Anonymoushttps://www.blogger.com/profile/17525961934302794120noreply@blogger.com