Re:Formalizing Text Editors in Coq
by jiggawatts on Tuesday June 09, 2020 @02:00AM
(#23464115)
Coming from a physics+CS background, I necessarily have some tolerance for greek symbols, especially when appropriate.
A good example is this gorgeous paper about grid-free methods for geometry processing: https://www.cs.cmu.edu/~kmcrane/Projects/MonteCarloGeometryP...
Yes, it uses greek symbols, but it's referencing mathematical concepts of geometry and the associated algebra. Hence, this is appropriate.
But that paper balances this out with illustrative diagrams and renderings. In full colour! Showing practical applications!
It's just beautiful. I wish more papers were like this one...
In Coordination2019 here is a lovely paper (W Kokke, J Garrett Morris, Philip Wadler.
Towards Races in Linear Logic) that uses emoji as formal notation. Maybe it could be the way to go? Like, if your formal language describes cars and buses, why not use and instead of alpha and beta?
Yes, a major from my many years in academia is sophistication is valued over simplicity. A bunch of fancy symbols and equations = important, so much of what is published appears, at least to me, to be much more complicated than it needs to be.
No, in that the sophistication, in the good cases, is because there is a multitude of subtletly and complexity in these subjects, as well as a formal framing of the issue so that it can be analyzed in an unambiguous manner. So, there is a reason for the obfuscation, although it mostly ingrown overkill at this point.
The best papers can both deal with the great complexity and sophisticated formalisms, while boiling it all down to an accessible delivery.
However, such papers are few and far between.