Formalizing Text Editors in Coq
arxiv.org
arxiv.org
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.
> 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.
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 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!
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.
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!
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.
However, such papers are few and far between.
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...
Using proper variable names still feels like cheating - as in how much easier it is to understand what the program does.
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.
Modeling work is important, but the pl community spends so much time modeling that they forget to value actually building things.
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.
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?
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.
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.
1. https://medium.engineering/why-contenteditable-is-terrible-1...
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).
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.)
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 :)
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
You can use https://www.arxiv-vanity.com/ to convert papers to HTML and read them in the browser though.