> Maths as written did seem pretty sloppy and not at all like a programming language whose expressions I could parse as I expected.

Look at Lean's mathlib: that's what fully formal mathematics looks like. It's far too verbose to be suitable for communicating with other people; you might as well try to teach an algorithms course transistor by transistor.