Hello. I want ask for your experience and opinion of proof assistants with “rich” type systems (allowing types dependent on terms and “proofs as terms, propositions as types”) like Agda and Coq. Specifically, how practical are these systems for pure mathematics, compared to HOL4 and HOL Light? Is there a significant advantage of these systems for pure mathematics compared to higher order logic?
Systems with types dependent on terms promise many expressibility built-it into the logic. My impression is that this is unnecessary and generates more problems than what it solves. When one tries to make the logic as rich as possible instead of as simple as possible, containing everything that could be desired built-in, the result is an enormously complex logic (with the implications that the logical kernel, if any, will be more difficult to verify either by ordinary code review or formally). In the case of Coq, it is my understanding that the logical foundation even changes regularly with new releases. Yet a system that has everything that could be wanted from it is an unachievable goal. Users or interested parties eventually find something missing so a process of endless revision of the foundations begins. This does not seem to happen with foundations based on set theory. ZFC (possibly augmented with proper classes and large cardinals) seems to be both sufficient for all mathematics and written in stone (in the sense that we are not continuously revising the foundations continuously). What is thus the motivation for the search for logical foundations and systems based on “rich” type theory (beyond higher order logic)? Setting aside philosophical interest in type theories (intuitionism), is there some advantage to them as foundations or practical systems beyond the built-in syntactic sugar? I am missing something? Thanks. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
