Dear Florin,
Thank you for your response. To clarify, I am a huge fan of calculation to work in mathematics. Just as I am a huge fan of using mathematics to study the world. However, it is important to recognize that simply using a tool is not enough: one has to use it well.
I can use mathematics to study love, quantifying as much as I can with numbers, say. But I don’t think that will get me very far. That’s not to say I can’t think closely and rationally about love, be organized, etc. I don’t simply have to throw it all to the wind. But the extreme abstractions of mathematics I don’t think are helpful.
Analogously, within mathematics, I want to use formalism for all the reasons we love (greater abstraction and clarity, the possibility of syntactic analysis to drive proof design, etc), but one has to recognize where it may not be appropriate. Even where it is appropriate, the question of how to formalize is a great intellectual act. That was my point of leading you to the EWDs and WFs. Almost everyone uses some sort of formalism to study logic, but the framework designed by Dijkstra and others took years to come to fruition, and the beauty and flexibility of that system shows the result of those years of careful thinking. It doesn’t suffice to just write down some symbols — not if you actually want to USE your formalism to calculate.
I have read many of Dijkstra’s experiments in geometry, admittedly many years ago. There is something there but they are far from encouraging. Similarly with other axiomatic approaches to geometry. If the goal is to streamline mathematical thought they haven’t gotten there yet! The amount of careful analysis and invention needed to prove simple theorems is tremendous. Does that mean the whole project is useless? No. It does mean that one has to keep going back to the original concepts and consider them, refine them, generalize them, and find the right patterns to pick out and try to subject to formalism. Towards that end, it is important to study really clean conceptual expositions of the field.
Looking forward to seeing your own experiments in geometry!
+j
PS. You reminded me that when I taught geometry I did use calculations to prove various things about angle and triangle congruence, parallel lines, etc.