4 ms·
That's the one I meant I think. It is nice, but as I said the impression it left me with was "you could have told me how the approach generally works sooner".
by mherrmann 7y ago
That's the one I meant I think. It is nice, but as I said the impression it left me with was "you could have told me how the approach generally works sooner".
- lonelappde 7y agoThat books wants to build the foundation (dependent types) before making the big claim in chapter 3. It's a bit weird because has Haskell shows, you don't need dependent types for basic theorem proving. (but dependent types do give a lot of useful power)
- dwohnitmok 7y agoWell 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.