I think there's a place for alternate representations like these outside of proofs that need to be exhaustively machine-checkable. I have, for what it's worth,

I think there's a place for alternate representations like these outside of proofs that need to be exhaustively machine-checkable. I have, for what it's worth, had far better experiences with Coq and the like than with mathematics in general.