Eusebia Sackman (Feb 28 2023 at 03:39): Eusebia Sackman (Feb 28 2023 at 03:39):It's interesting how proof assistants based on type theory are more widely used, even though I haven't personally come across any convincing arguments in favor of type theory. However, the people I've spoken to about this topic might not have a deep understanding of type theory. If I were to ask people who are more knowledgeable about it, I might get better answers. As someone who is not well-versed in type theory, I find ZF set theory easier to understand than type theory. It seems that a lot of the work involved in developing a proof assistant is focused on features like editor support and tactics, rather than the foundational theory. As a Coq user, I don't need to directly interact with the type theory; instead, I study existing Coq code to learn from patterns and apply them to my own work. I don't need to memorize things like Greek letter conversions or type motives. If the choice of foundational theory doesn't significantly impact the user experience, then it's interesting to consider why type theory remains more popular.
Paolo Giarrusso (Feb 28 2023 at 04:56):https://mathoverflow.net/q/376839/36016 is probably relevant on the topic.
Karl Palmskog (Feb 28 2023 at 07:32):if someone actually prefers ZF set theory, I'd honestly advise them to go with Isabelle/ZF. You can do (axiomatic) set theory just fine in Coq like in Gaia, but it will never feel like regular set theory.
Patrick Nicodemus (Mar 01 2023 at 00:25):Formalization of the Fundamental Group in Untyped Set Theory Using Auto2
https://dl.acm.org/doi/abs/10.1007/s10817-018-9478-0
Notification Bot (Mar 02 2023 at 19:55):A message was moved from this topic to #Miscellaneous > Mizar by Karl Palmskog.
Last updated: Oct 04 2023 at 22:01 UTC