Survey of languages for formalizing math :: Cezary Kaliszyk
Observation: The language of formal systems is not the way mathematicians actually communicate (in person verbally, in writing).
Computer Algebra Systems (CAS) and Proof Assistants are viewed as "code" separate from Natural Language.
Natural Language Processing (NLP) of math does not recognize repeated use of the same notation, whereas humans recognize that as a convention.
Aspects that distinguish formal from informal communication: types, inheritance, equality (isomorphism). Each of those aspects are typically implicit for human consumers.
The goal of formal specification is proof, whereas in informal communication the goal is to convince the reader. Those are distinct.