News for hackers. Stuff that matters.
Re:Formalizing Text Editors in Coq by jiggawatts on Monday June 08, 2020 @09:13PM (#23462599)
This. This is the problem with academia in a nutshell.

I get mercilessly downvoted whenever I point out that it makes zero sense to use Greek letters in computer science papers. There is no rich history of Ancient Greek computer science that is being referenced for consistency with the new research!!! It's 100% intellectual wankery, nothing more.

I experienced the same thing first-hand with AI research. Nobody is going to get published for using a straightforward numerical approach like Automatic Differentiation in a paper, so they spend 90% of their effort symbolically differentiating the formulas and end up with something that is numerically unstable but oh so pretty and impressive looking when laid out with LaTeX.

Publishing in science is now all about showing off, and not at all about the advancement of science. It's politics, not practice.

PS: Go back and compare CS papers published in the 60s, 70s, and even 80s with stuff being put out now. It's night & day!

Re:Formalizing Text Editors in Coq by throwawaygh on Monday June 08, 2020 @09:28PM (#23462692)
Hm. I don't really care about using greek letters per se. That's just a colloquialism for unnecessary formalism.

Any critique of AI is fair, though. If you think PL theory is bad, try running the code from a good 90% of neurips papers. Hearing ML people complain about the reproducibility of psych research is hilarious.

Like, at least their reproducibility problem makes an iota of sense. Empirical research involving humans is inherently messy. Doesn't excuse anything, ofc, but I at least understand why the problem could be methodology rather than outright fraud. With neurips papers, I'm literally just trying to run published code using their install scripts on the exact instance of an AWS machine they said they used, and getting just fucking absolutely wildly different numbers.

Either I'm totally incompetent after 20 years of coding and publishing, or the deep learning reproducibility meltdown is going to make the psych reproducibility crisis look like a minor blip.

It's so hard for CS Researchers to write comprehensible code that does something new and actually works. I originally said "I'll never understand why", but I guess my above comment explains it perfectly: after a couple rounds of peer review, people get the picture and learn to stop writing working good explanations of working code.

Re:Formalizing Text Editors in Coq by yters on Monday June 08, 2020 @10:24PM (#23463023)
Yes and no.

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.

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...

Re:Formalizing Text Editors in Coq by lou1306 on Tuesday June 09, 2020 @05:17AM (#23465042)
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?
Re:Formalizing Text Editors in Coq by lou1306 on Tuesday June 09, 2020 @11:05AM (#23467270)
(The above comment ended with "why not use :car and :bus instead of alpha and beta?". Apparently HN does not support emoji?)
Re:Formalizing Text Editors in Coq by z3t4 on Tuesday June 09, 2020 @05:45AM (#23465161)
When I started programming I used only single letter variables.

Using proper variable names still feels like cheating - as in how much easier it is to understand what the program does.