[bor0]

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]

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]

No offence taken! Your first comment was constructive. I am looking forward to make the paper better.

[p4bl0]

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]

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!