3 ms·

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

by 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!

by bor0 6y ago

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!