On the one hand:
Ratdolt's 1482 editio princeps (albeit of a Latin translation of an Arabic translation) labels points with lower case letters.
Herwegen's 1533 editio princeps of the original Greek text also labels points with lower case letters.
Moreover, for instance, as late as 1565, a corrected edition of Commandino's Latin translation of Archimedes still labels points with lower case letters. One might well argue that this continues the manuscript tradition, as exemplified by the Codex Vaticanus.
On the other hand, just a few years later:
Billingsley's 1570 English translation labels points rather with upper case letters.
Commandino's 1572 Latin translation labels points with upper case letters.
Clavius's 1574 Latin translation labels points with upper case letters.
So, writing admittedly as a complete layman with regards to the textual transmission of Greek Mathematics, I would suggest that the custom of labelling points with upper case letters might well be an innovation of mid-late 16th century publishing, and that it in any event demonstrably has nothing to do with the earliest printed editions and the manuscript traditions they would have derived from.
From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. (It would be very interesting to study how to formalize this kind of convention -- it's something common in mathematical practice missing from proof theory.)
I have written proofs in this style, and once taught it to students. I find that this system -- or indeed any variant of natural deduction -- is extremely valuable for teaching proof to students, because it associates to each logical connective the exact mathematical language needed to use it and to construct it. This is particularly helpful when you are teaching students how to manipulate quantifiers, and how to use the axiom of induction.
When doing proofs myself, I find that this kind of structured proof works fantastically well, except when working with quotients -- i.e., modulo an equivalence relation. The reason for this is that the natural deduction rules for quotient types are rather awkward. Introducing elements of a set modulo an equivalence relation is quite natural:
$$
\frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}}
{\Gamma \vdash [e]_R \in A/R}
$$
That is, we just need to produce an element of $A$, and then say we're talking about the equivalence class of which it is a member.
But using this fact is rather painful:
$$
\frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B}
$$
This rule says that if you know that
- $e$ is an element of $A/R$, and
- $t$ is some element of $B$ with a free variable $x$ in set $A$, and
- if you can show that for any $x$ and $y$ in $R$, that $t(y) = t(z)$ (ie, $t$ doesn't distinguish between elements of the same equivalence class)
Then you can form an element of $B$ by picking an element of the equivalence class and substituting it for $x$. (This works because $t$ doesn't care about the specific choice of representative.)
What makes this rule so ungainly is the equality premise -- it requires proving something about the whole subderivation which uses the member of the quotient set. It's so painful that I tend to avoid structured proofs when working with quotients, even though this is when I need them the most (since it's so easy to forget to work mod the equivalence relation in one little corner of the proof).
I would pay money for a better elimination rule for quotients, and I'm not sure I mean this as a figure of speech, either.
Best Answer
Hardy's opposition was to the Mathematical Tripos (the Cambridge undergraduate mathematics degree), as it was prior to its reform in 1909, which Hardy did much to bring about.
The text of "A Mathematician's Apology", with Snow's preface, is here; the relevant paragraphs are
As for why Hardy was so much against it, Snow's preface gives some of the reasons. It was a system which heavily emphasised fluency in intricate calculations rather than conceptual understanding. It was also a very rigid system which was slow to incorporate new developments in the subject (particularly those originating outside Britain). Moreover, the way the examination questions were set prioritised separating the top handful of candidates, rather than testing whether candidates near the bottom end had grasped the essentials (according to the statistics quoted on the Wikipedia page, in the 1854 examination the cut-off mark for a first-class degree was about 10% of the total marks available, and the cut-off for a third-class was about 2% -- seriously!).