zozbot234 4 days ago

Thanks for the reference! That take of his sounds a bit confused in-context (univalence and constructivism are not directly related, you can work non-constructively and still use the overall featureset of HoTT/univalence) but then his remark about how he's just working on non-constructive stuff that we don't even know how to phrase constructively is just fair.

Relatedly, the kind of philosophical constructivism that would make claims like "non-constructive mathematics is just wrong and useless" has been a bit problematic in many ways, he's not totally off-base about this.

I disliked his skepticism about proofs-as-programs the most, but that's because I think "a direct proof is a program" is very much a worthwhile statement. Of course some mathematicians will opt not to care about that.

Reply View 0 replies