4 ms·
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
by 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 agoNo offence taken! Your first comment was constructive. I am looking forward to make the paper better.
- p4bl0 6y agoI 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.