> Now that's a fine thing in a computer language -- and there are philosophers who say mathematical truth is no more than computation. But mathematical notation is for humans to talk about things that have meanings that humans can understand.
Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation?
You can look up the definition of each function and learn precisely what it does, without ambiguities. You can open up a debugger and trace every step of the algorithm. Source code tends to be formatted to emphasise its division into units that can be analysed separately. Even if the code uses a framework you don't recognise, you can probably understand some of the underlying logic just fine, thanks to a consistent syntax and (often) descriptive function names.
In a mathematical paper, often there's some notation that isn't defined and there isn't even any pointer where to look for definitions. Important objects are given one-letter names. Theorems are often only numbered; good luck remembering what lemma 2.17.3b was about. Proofs are written in prose (instead of something like Leslie Lamport proposed[0]). You have to fill in conceptual gaps and remind yourself of unstated assumptions. Notation and terminology is often ambiguous — what does "exponential time" mean? Is it DTIME(2^(c*n)) or DTIME(2^polynomial(n))? Does "increasing" mean "strictly increasing" or "non-decreasing"? Is zero a natural number? And so on.
A mathematical formalism that could be interpreted in a purely mechanical way would be a huge improvement.
Indeed, looks like scientific literature in general and mathematical literature in particular are stuck in the past century. As much as I enjoy reading printed materials, I often think that using a modern computer-based approach to presenting them could prove a lot superior. And no, PDF would not cut it, even with the possibility of hyperlinking. In my view, PDF is like the idea of the horseless carriage, or, rather, of a carriage pulled by a mechanical horse - a new technology stuck in the past. Looks like the modern web browser platform, on the other hand, could provide a reasonable base on which one could build an extremely powerful "IDE" for creating and interacting with mathematical expositions.
> Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation?
This is clearly subjective. I read lots of mathematics research that I find more accessible than even pretty mundane source code (and yes, I write software for a living and have done so for over ten years).
I feel obliged to point out that HoTT is… really rather abstract. I'm just starting to learn about it now in my spare time, and I hold a master's degree in mathematics specialising in logic.
The answer to all of your questions: computer programs are written for computers to understand, and computers aren't very smart. Mathematical papers are written for mathematicians to understand, and they tend to be a lot smarter than computers.
Machine language is also written for computers to understand, but it's not easy to read. Computer-formalized math is usually even harder to read than regular notation. I don't think computers have much to do with this.
True, I should have said it better as, programming languages are written for compilers to read, and they're not very smart. Machine language is written for computers themselves. Computer-formalized math I don't think is written for anyone to read.
Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation?
You can look up the definition of each function and learn precisely what it does, without ambiguities. You can open up a debugger and trace every step of the algorithm. Source code tends to be formatted to emphasise its division into units that can be analysed separately. Even if the code uses a framework you don't recognise, you can probably understand some of the underlying logic just fine, thanks to a consistent syntax and (often) descriptive function names.
In a mathematical paper, often there's some notation that isn't defined and there isn't even any pointer where to look for definitions. Important objects are given one-letter names. Theorems are often only numbered; good luck remembering what lemma 2.17.3b was about. Proofs are written in prose (instead of something like Leslie Lamport proposed[0]). You have to fill in conceptual gaps and remind yourself of unstated assumptions. Notation and terminology is often ambiguous — what does "exponential time" mean? Is it DTIME(2^(c*n)) or DTIME(2^polynomial(n))? Does "increasing" mean "strictly increasing" or "non-decreasing"? Is zero a natural number? And so on.
A mathematical formalism that could be interpreted in a purely mechanical way would be a huge improvement.
[0] http://research.microsoft.com/en-us/um/people/lamport/pubs/p...