6 ms·

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

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.

bor0 6y ago
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.
- p0llard 6y ago
  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!
  - bor0 6y ago
    No offence taken! Your first comment was constructive. I am looking forward to make the paper better.
  - p4bl0 6y ago
    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.
- unixhero 6y ago
  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!
throwawaygh 6y ago
> ...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.
- jiggawatts 6y ago
  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!

bor0 6y ago

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.

p0llard 6y ago
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!
- bor0 6y ago
  No offence taken! Your first comment was constructive. I am looking forward to make the paper better.
- p4bl0 6y ago
  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.
unixhero 6y ago
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!

throwawaygh 6y ago

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

jiggawatts 6y ago
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!