Hacker News Reader

Which tutorial did you use? As someone coming from computer science, I found https://leanprover.github.io/theorem_proving_in_lean/ very approachable as an introduction to ITP in general.

View on HN

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".

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)

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.

Reply on news.ycombinator.com