[FOM] Structural set theory for proof assistants

[Joshua Chen]

Dear FOM,

As part of my PhD I work with multiple proof assistants, and have
recently been wrangling with Mizar and its idiosyncracies. This got me
considering what a modern set theory-based proof assistant might do
differently, and in particular if, instead of material set theory, we
might choose to base such a system on structural set theory. I've
started a formalization of Mike Shulman's SEAR in Isabelle on top of
triply-sorted first-order logic, and will be experimenting to see how
much mathematics I can formalize in this.

Not being an expert, I'm posting here to ask:

Have structural set theories been considered as foundations for formal
*computer* mathematics before? Maybe some people who know the details of
these foundations, and have perhaps tried to work out some mathematics
in them, could comment on the prospects of such an undertaking? Even the
more recent developments in set-theoretic systems seem to mostly use
ZF(C), and I would like to know if this is a historical/cultural
accident, or if there is some deeper obstruction.

Best regards,

Josh

-- 
Joshua Chen

Computational Logic
Department of Computer Science
University of Innsbruck

Email: fom at joshchen.io
Web: https://joshchen.io