search

isovector / reasonablypolymorphic.com

⏳ my math blog
http://reasonablypolymorphic.com
BSD 3-Clause "New" or "Revised" License
23 stars 11 forks source link

blog/cbc-report10/index #42

Open utterances-bot opened 10 months ago

utterances-bot commented 10 months ago

Certainty by Construction Progress Report 10 :: Reasonably Polymorphic

https://reasonablypolymorphic.com/blog/cbc-report10/index.html

artimath commented 10 months ago

Sandy, would it make any sense at all in the world to utilize Agda as a learning tool? Say if I had the ambitious desire to achieve a graduate level understanding of many pure math concepts? Would proving theorems and such in Agda (or haskell) provide benefit beyond traditional approaches?

Next level: If I wanted to acquire same level of understanding but approaching math via Type Theory rather than Set Theory, would Agda and such be a help or a hindrance?

Or am I thinking about this entirely wrong?

Just a curious random late night question.

isovector commented 10 months ago

Hi Ryan,

Great questions! I'm obviously biased here, but I've found using Agda has dramatically improved my understanding of mathematics---mostly due to the fact that while it's easy to fool myself into thinking i understand, the computer is much less easily duped.

Agda lets me reharness my programming skills towards learning math, and it turns out many theorems happen to be the only thing that typechecks.

More controversially, i think set theory is mind poison, in that it seems to encourage people to ask all sorts of ill-typed questions. I suspect if we had type theory first, and set theory came along later, nobody would be clamoring to switch.

Best, Sandy

On October 22, 2023 12:22:54 a.m. PDT, Ryan Hunter @.***> wrote:

Sandy, would it make any sense at all in the world to utilize Agda as a learning tool? Say if I had the ambitious desire to achieve a graduate level understanding of many pure math concepts? Would proving theorems and such in Agda (or haskell) provide benefit beyond traditional approaches?

Next level: If I wanted to acquire same level of understanding but approaching math via Type Theory rather than Set Theory, would Agda and such be a help or a hindrance?

Or am I thinking about this entirely wrong?

Just a curious random late night question.

-- Reply to this email directly or view it on GitHub: https://github.com/isovector/reasonablypolymorphic.com/issues/42#issuecomment-1774018471 You are receiving this because you are subscribed to this thread.

Message ID: @.***>

artimath commented 10 months ago

Sandy, thank you for your answer!

Simple question... is proving theorems via Agda equal to or 'isomorphic' ;) to using type theory instead of set theory?

Or can one intentionally, or unintentionally, recreate set theory via the types in Agda?

In other words, if I proceed with using Agda as I learn mathematics, will I essentially be operating from a type-theory baseline rather than set-theory?

I'd google the above question normally, but it's sorta esoteric and thought you'd have a easy answer.

Thank you! Really enjoying Certainty by Construction.

isovector commented 10 months ago

The things you can prove in Agda/type theory are a subset of the things you can prove in set theory, because TT is stronger and thus requires more from a proof (in particular, well-typedness, and usually constructiveness.)

Of course, you can always just postulate things that you can't prove directly, and then move forwards, so this is not a real limitation in practice.