Re:The Future of Mathematics? [video]
by mherrmann on Wednesday October 09, 2019 @11:50AM
(#21204327)
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".
[ Parent
| on HN ]
Re:The Future of Mathematics? [video]
by lonelappde on Wednesday October 09, 2019 @03:51PM
(#21207210)
That 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)
Re:The Future of Mathematics? [video]
by dwohnitmok on Wednesday October 09, 2019 @10:05PM
(#21210203)
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.