7 ms·

Formalizing Text Editors in Coq

85 points by gbrown_ 6y ago

benrbray 6y ago
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/ https://prosemirror.net/
- edjroot 6y ago
  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.) [1]: https://github.com/Ionaru/easy-markdown-editor https://github.com/Ionaru/easy-markdown-editor
  - benrbray 6y ago
    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 :)
p0llard 6y ago
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!
jkaptur 6y ago
Interesting to contrast this with [1], which works on formalizing rich text editors (for HTML). 1. https://medium.engineering/why-contenteditable-is-terrible-122d8a40e480 https://medium.engineering/why-contenteditable-is-terrible-1...
_pmf_ 6y ago
Is Emacs vs. Vi decidable?
- kabdib 6y ago
  Only with a choice of weapons. :-)
- nurettin 6y ago
  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.
firstbabylonian 6y ago
Are there any open source libraries that implement this in practice?
sanxiyn 6y ago
It would be interesting to prove an implementation using gap buffer, against the same specification.
- neel_k 6y ago
  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 https://github.com/pigworker/CS410-15
emj 6y ago
I wish arxiv could be more like a blogging platform with standards and less a PDF repository.
- p4bl0 6y ago
  ArXiv has the LaTeX source for most of the papers they host. They could compile it to HTML, but it might be quite difficult in some cases.
- elcomet 6y ago
  Arxiv is a pre-print platform for scientific publications, not a blogging platform. Other platforms are designed for this, such as medium. You can use https://www.arxiv-vanity.com/ https://www.arxiv-vanity.com/ to convert papers to HTML and read them in the browser though.

85 points by gbrown_ 6y ago

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/ https://prosemirror.net/

edjroot 6y ago
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.) [1]: https://github.com/Ionaru/easy-markdown-editor https://github.com/Ionaru/easy-markdown-editor
- benrbray 6y ago
  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 :)

p0llard 6y ago

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!

jkaptur 6y ago

Interesting to contrast this with [1], which works on formalizing rich text editors (for HTML). 1. https://medium.engineering/why-contenteditable-is-terrible-122d8a40e480 https://medium.engineering/why-contenteditable-is-terrible-1...

_pmf_ 6y ago

Is Emacs vs. Vi decidable?

kabdib 6y ago
Only with a choice of weapons. :-)
nurettin 6y ago
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.

firstbabylonian 6y ago

Are there any open source libraries that implement this in practice?

sanxiyn 6y ago

It would be interesting to prove an implementation using gap buffer, against the same specification.

neel_k 6y ago
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 https://github.com/pigworker/CS410-15

emj 6y ago

I wish arxiv could be more like a blogging platform with standards and less a PDF repository.

p4bl0 6y ago
ArXiv has the LaTeX source for most of the papers they host. They could compile it to HTML, but it might be quite difficult in some cases.
elcomet 6y ago
Arxiv is a pre-print platform for scientific publications, not a blogging platform. Other platforms are designed for this, such as medium. You can use https://www.arxiv-vanity.com/ https://www.arxiv-vanity.com/ to convert papers to HTML and read them in the browser though.