[HN Gopher] Formalizing Text Editors in Coq ___________________________________________________________________ Formalizing Text Editors in Coq Author : gbrown_ Score : 23 points Date : 2020-06-08 08:15 UTC (14 hours ago) (HTM) web link (arxiv.org) (TXT) w3m dump (arxiv.org) | benrbray wrote: | 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). | | [1]: https://prosemirror.net/ | p0llard wrote: | 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 wrote: | 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. | throwawaygh wrote: | _> ...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" paper. Meanwhile, POPL proceedings for | 20+ years have been littered with 2 pages of substance and 18 | pages of greek-letter-masturbation. The only thing that will | ever push the field forward is _working and well-explained | /documented code_. But hacking out some lines of ocaml/gallina | isn't valued as much as hacking out lines of \Gammas and | \vdashes. Smart people realize that quickly and either get out | or learn how to write 1+1=2 in a super complicated way. | | 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. IMO. | jkaptur wrote: | Interesting to contrast this with [1], which works on formalizing | _rich_ text editors (for HTML). | | 1. https://medium.engineering/why-contenteditable-is- | terrible-1... ___________________________________________________________________ (page generated 2020-06-08 23:00 UTC)