[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)