Hacker News new | past | comments | ask | show | jobs | submit login

Well if you just have Haskell 2010 types, you're talking about really really basic theorem proving since all you have is propositional logic. The most interesting thing I can think of to prove with Haskell 2010 types is (the constructive version of) de Morgan's laws. Almost all other interesting mathematical statements are out of reach.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact