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.
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.
> 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.
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, 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.
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?
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.
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.
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 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?
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!
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.
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!
Neat! It would be great to have a universally agreed-upon standard for how text editors behave (especially with regard to embedded / structured content, cursor position, etc.) and which operations they should support.
I recently came across ProseMirror [1], which seems to be a fantastic step in this direction. I've been experimenting with using it to build a Markdown editor with better support for math and pre-defined HTML blocks (for e.g. stating theorems, corollaries, etc. in math notes).
Indeed, ProseMirror is highly regarded by its code quality, just as its older sibling, CodeMirror. It even raised quite a bit of money on Indiegogo.
Are you planning on open-sourcing your editor? I'd love to use something like this on a project of mine. (I currently use the much less ambitious EasyMDE [1], which is based on CodeMirror.)
Yes, that's the plan! I've long lamented that editors like Typora and Roam are closed-source, preventing users like me from tweaking them to my specific use-case. So I'm hoping to build something that others can modify if they need to.
My priorities are math support, citations/wikilinks and the ability to define custom document structure (theorems, etc.). I basically want users to be able to specify a ProseMirror schema with CSS to go along with it.
Can I ask about your specific use case? Any features you've been really missing? No promises they'll make it in, but I'm curious :)
Gap buffers are zippers, which makes this particular case really easy: they arise as derivatives of the list functor, and so for generic categorical reasons they are isomorphic to a list plus a position in it. This means you can prove things about lists-with-positions and basically automatically transport them to statements about gap buffers.
The specification in this note is not an ideal top-level spec, though: it just says there are a series of editor commands that can change one string into another. This is just a basic sanity check, but you can't do much more than that here because the editor state is too impoverished -- it's just the current string.
However, there is an interesting line of attack in (1) enriching the state enough to easily model richer things like command history and undo (eg, by making the state be the whole history of documents and commands), (2) giving each update command a semantics in terms of simple whole-state changes on the enriched state, and then (3) showing that a more efficient representation correctly implements the simple whole-state semantics.
About five years ago, Conor McBride taught a course on dependently-typed programming in Agda in which one of the projects was implementing provably correct text editors, using zippers/gap buffers and interaction via Mealy machines. The link is: https://github.com/pigworker/CS410-15
As someone who saw the war happen back in early 2000s, vim conceded almost immediately (because it was the efficient move). And people still can't get over the fact that users continue to use vim anyway.
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.