> Formalisms can be impractically formal. The level of precision required by machines is beyond even what most mathematicians are used to casually (i.e., pen an

> Formalisms can be impractically formal. The level of precision required by machines is beyond even what most mathematicians are used to casually (i.e., pen and paper, or at a blackboard). If you had to do math like you write code, mathematicians would go bonkers. Include this, type-cast that, ... nah, everyone knows what this and that is supposed to mean, right? Mathematics only looks formal: compared to software it is really another natural language -- because its purpose is to communicate between humans, whereas software is ultimately not about communication but design of artifacts. The point about practicality still holds though, but since the purposes are different it must be something of a different kind of practicality to aim at.