> It is incredibly common in mathematics to silently "convert" objects between different types. [..] silently identifying isomorphic objects
Would you agree that correct instances of this pattern are exactly cases of considering objects only up to isomorphism? The problems of equality in constructive mathematics is a complicated one but things are starting to clear out, with constructive interpretations of this pattern (eg constructive models of univalence, implemented in cubical agda) people are starting to do wonders, like this superb grad thesis about finiteness [1].
The hard part is certainly the silentness of these identifications (which if i'm not mistaken is kind of the difference between extensional and intensional logics). But again i believe that they can be systematized contextually: one could for example declare in a preample which implicit isomorphisms they are going to use, which would then be disambiguated by type and decidably searched-for.
> ignore certain things [..] basically all the common notational shorthands
This is certainly a challenge for formalization, but my belief is that it can be done. Imho this is where the cross-pollination between "real-life programming" and constructive maths shows: contextual generalization (binding) of unbound variables (eg implicit polymorphism in ML-likes types, structure inference and coercions along structure refinements using typeclasses/search-like procedures and unification hints, ...). We definitely have to continue developing nice "surface languages" for generating proofs (compiling?) in the formal core (assembly?).
> Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers.
I'm not sure i understand your point: constructive models of real number exist (usually as equivalence classes of some kind, which a sufficiently sophisticated type theory will give you tools to work with). Constructive models doesn't mean we have a decidable normalization procedure tho. I skimmed through it but there is this recent talk at msp101 about real numbers in agda [2] and there is a chapter about it in the HoTT book.
Would you agree that correct instances of this pattern are exactly cases of considering objects only up to isomorphism? The problems of equality in constructive mathematics is a complicated one but things are starting to clear out, with constructive interpretations of this pattern (eg constructive models of univalence, implemented in cubical agda) people are starting to do wonders, like this superb grad thesis about finiteness [1].
The hard part is certainly the silentness of these identifications (which if i'm not mistaken is kind of the difference between extensional and intensional logics). But again i believe that they can be systematized contextually: one could for example declare in a preample which implicit isomorphisms they are going to use, which would then be disambiguated by type and decidably searched-for.
> ignore certain things [..] basically all the common notational shorthands
This is certainly a challenge for formalization, but my belief is that it can be done. Imho this is where the cross-pollination between "real-life programming" and constructive maths shows: contextual generalization (binding) of unbound variables (eg implicit polymorphism in ML-likes types, structure inference and coercions along structure refinements using typeclasses/search-like procedures and unification hints, ...). We definitely have to continue developing nice "surface languages" for generating proofs (compiling?) in the formal core (assembly?).
> Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers.
I'm not sure i understand your point: constructive models of real number exist (usually as equivalence classes of some kind, which a sufficiently sophisticated type theory will give you tools to work with). Constructive models doesn't mean we have a decidable normalization procedure tho. I skimmed through it but there is this recent talk at msp101 about real numbers in agda [2] and there is a chapter about it in the HoTT book.
[1] https://doisinkidney.com/posts/2021-01-04-masters-thesis.htm...
[2] http://msp.cis.strath.ac.uk/101/slides/2021-06-10_bob.pdf