Hacker News Reader

Comment by opus132 | Hacker News Reader

This looks more like someone proved some trivial lemmas about lists and wrote the simplest possible DSL to do some list manipulations rather than anything close to resembling a serious piece of work on formally verified text editors.

This is first-lecture-learning-Coq level stuff to be completely honest; it's interesting if you've never seen Coq before, but it's not really what it claims to be at all. The amount of work to go from this to "formalizing full-nlown text editors, such as vim" is enormous.

If we remove the proof scripts (and duplicated statements of Lemmas/Theorems in Gallina and mathematical notation) since these would never be included in a published paper (only as an accompanying artefact unless a novel tactic/proof scripting method is the actual topic of the paper), the length of the paper almost halves and the amount of substance becomes clearer.

View on HN

> ...the amount of substance becomes clearer

IMO this attitude is why formal methods based on proof assistants never took off.

That entire PL theory research community seems to think that implementation work is unimportant and not even worth a few page "tools/casestudy" workshop paper. Even a tiny four page write-up gets a "why isn't this a homework assignment" style response.

That, by itself, is I guess not terrible. But POPL proceedings for 20+ years have been littered with 2 pages of substance and 18 pages of greek-letter-masturbation. Most of those papers build insanely complex calculi to capture a simple idea that every junior engineer can understand in half a day. And this complaint always fell on deaf ears. At least, as long as the author was able to say "logical relations" or "linear types" or whatever the hell keywords y'all are applying your elimination rules on these days.

The only thing that will ever push that field forward is shitloads of working and well-explained/documented code. But hacking out some lines of ocaml/gallina (or, god forbid, Python/C++... if I have to listen to an SML acolyte complain about parallelism in Python one more time...) isn't valued as much as hacking out lines of \Gammas and \vdashes. Taking the time to explain short code examples gets you "that's a homework problem" responses. As if explaining a digestible piece of code concisely is some sort of admission of intellectual impotence. Smart people realize this quickly and either get out (if they want to have an impact on the world) or learn how to write 1+1=2 in a super complicated way (if they just want that piece of paper).

Anyways, you're right. The paper is a far cry from "formalizing a text editor in coq". But the "your implementation work doesn't deserve my time or attention" attitude is a big reason why this research community hasn't really had much impact even after several decades of outsized investment. IMO.

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!

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.

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.

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?

(The above comment ended with "why not use :car and :bus instead of alpha and beta?". Apparently HN does not support emoji?)

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.

> Most of those papers build insanely complex calculi to capture a simple idea that every junior engineer can understand in half a day.

Except that is working code. The insane complexity is almost never in the calculi themselves, but rather in the proofs that go along with them, to clearly show why the approach that has been taken to formalize that "simple idea" works as expected. That modeling work is quite essential if you want to ensure that the "simple" features in a programming language interact together in a sensible and useful way.

Working code has the important attribute of being executable. Inference rules aren’t executable.

Modeling work is important, but the pl community spends so much time modeling that they forget to value actually building things.

Thanks, that needed to be said. Hopefully not all research communities are alike, and the behavior will be very different in the security/privacy community for example. That is part of the reason why I work in the latter field rather than in PL.

Also, I really enjoyed this paper for the exact reasons that GP disliked it: it is short and understandable even with very remote and vague souvenirs or Coq.

As far as I understand, GP meant that this piece should be in an article or blog post form because it has very beginner material for the PL community.

Checkout Lean, the lead developer also started Z3 . Lean 3 is implemented in C++ and apparently is much faster than Coq. They are in the process of implementing Lean 4, which will feature native code generation and might become one of the first practical dependently typed programming languages.

Lean 3 is community maintained, aka dead. Lean 4 is described as "go away", and it will be incompatible with Lean 3. So much for practicality.

> Lean 3 is implemented in C++ and apparently is much faster than Coq.

1. The parent didn't comment in any way on Coq's performance, they barely mentioned Coq at all.

2. Coq is implemented in OCaml, which produces pretty good code. If Lean is faster than Coq, that's more likely due to more optimized algorithms or data structures.

3. Your wording using "apparently" suggests that you don't even have practical experience with this, you just want to promote a software system you have never used?

What is the point of a comment like this?

Proof drives understanding of your code. That is why the resulting code is often small and clear. It pushes the field forward, but not in the direction you might think it does.

You see, the shitloads of working code really works and solves problems. But you might not understand why. The work with proofs gets you closer to an understanding of the underlying why-question.

And I don't think PL-research will ever catch up to the real-world experiments done in code. It took 40 years to embrace garbage collection for typical programs, so I don't have hope anything else will move soon.

> formal methods based on proof assistants never took off

A few examples of large scale industrial projects using formal assistants:

seL4: A proven correct commercial OS used in billions of mobile devices.

CompCert: A proven correct C compiler used by Airbus for avionics software.

ARM: End-to-end verification of CPUs (https://alastairreid.github.io/papers/CAV_16).

There are many more.

Hi! Author here. First of all thanks to whoever shared this on HN, it was amazing to see it on the front page :)

> but it's not really what it claims to be at all

I agree that the content may be interesting (only) to Coq newcomers, but I disagree with the quoted statement.

If you extract the code to Haskell e.g., and put some IO handling you basically have a line editor.

> the length of the paper almost halves and the amount of substance becomes clearer

Thank you for this. I can amend it in a future version once I get more/other comments on the paper.

My comment regarding "substance" was rather snarky, and I apologise for that.

I suppose the point I was really trying to make is that whilst this is certainly a nice demonstration of how to prove properties of data structures in Coq, actually specifying and verifying vim would be a monumentally larger task, and critically, most of the effort would be in entirely different areas.

I should have phrased this better though and my tone was way off, so I'm sorry if my first comment caused offence; anyone promoting formal methods to the SE community at large is doing a great thing!

No offence taken! Your first comment was constructive. I am looking forward to make the paper better.

I just wanted to express my appreciation of this reply. I originally wrote a simple ":)." but it's not really how it works here on HN :). Anyway, thanks for not being stubborn and pedantic, this is part what makes most of HN nice.

Hi!

I am a 100% newcomer to the world of formal proofs and certainly dont know Coq. Because your topic was down to earth and the proof you provided were simple, I was able to understand these proofs. As such your paper made me aware of how this community builds papers and proofs, and I can understand how this will grow insanely in complexity. Thank you!

Reply on news.ycombinator.com