<div dir="ltr"><div>In this nice quote, foundations are considered from the perspective of expressive power:</div><div>  What if we find mathematics that *cannot* be formalized with our choice of foundations?</div><div>In our experience with proof assistants, the discussion is generally not about expressive power (the possibility to formalize something at all) but about convenience, which in practice determines feasability:</div><div>  What if we find mathematics that cannot be formalized *in practice* by our proof assistant, due to our choice of foundations?</div><div><br></div><div>It is not obvious to me whether this impact of foundations  on practical usability of proof assistants is going to stay, or whether it is a problem of youth that will go away as we develop better assistants. I would rather hope the latter: that we can build proof assistants that are flexible enough to conveniently support a very broad range of mathematics.<br></div></div>