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

Attachment: 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

Reply via email to