Perhaps it would make more sense to ask people who are using rich type
systems what their motivations are :)
(On this list it's probably mostly people who are satisfied with simple
type theory.)
On 15 September 2017 at 11:06, Mario Castelán Castro <marioxcc...@yandex.com
> wrote:
> 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
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
>
------------------------------------------------------------------------------
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
