Hacker News Reader

Comment by erichocean | Hacker News Reader

FWIW, I'm not mathematically-inclined and haven't found Coq to be painful to use. As soon as I really want verified code, doing stuff in Coq seems like the easiest path because the proof automation tooling is pretty great, especially if you follow the approach in Certified Programming with Dependent Types[0].

I also like Alloy[1] for messing around with logical data structure definitions interactively.

[0] http://adam.chlipala.net/cpdt/

[1] http://alloy.mit.edu/alloy/

View on HN

I think the pain only appears when you start trying to do "deep specification" of large systems. My research group has about 5-10 of us that have all built large systems (5-60 kloc) and verified them in Coq. I know each of us long list of gripes with the tooling.

My recent work has been on a verified JIT compiler and having to write tactics and lemmas to deal with facts about bit vectors seems stupid when SMT solvers are particularly good at this kind of reasoning.

When you say that you verified a large system in Coq, in what language did you write your system? does it mean that your language semantics has do be defined in Coq, or did you write your system using Coq as a programming language?

I'm with you that, depending on the problem, different verification approaches make the most sense. I wish it was easier to combine results from different tooling.

I thought about trying Alloy since in not mathematical enough for HOL, etc. An EAL7 VPN project used it too, IIRC. Do you have a link to a tutorial or reference for how you apply it to data structure def's?

Another interesting tool is ProB[1]. I believe it does symbolic model checking and supports partial order reduction. It works on specifications in multiple languages, including TLA+, but I haven't had the chance to use it myself because it doesn't support all TLA+ features. In particular, it doesn't support TLA+'s higher-order operators, which my specifications use.

[1]: Cool visualizations: https://www3.hhu.de/stups/prob/index.php/State_space_visuali...

Appreciate the reference. I'm holding off on ProB and B for now because the B method has mixed results in CompSci literature. I mean, it's been proven on a number of high assurance projects by pro's. I at least like that both B and TLA+ are pretty straight-forward to compared to most where a person has both a mathematical and good, mental model of what's going on. B particularly as it maps to imperative with ease.

I'm keeping it bookmarked just in case. Meanwhile, I just got a ton of stuff on asynchronous verification in response to another commenter's troubles there. I was away too long: looks like async and GALS are both mostly solved problems at the cutting edge with some tools to help. A lot to skim or read that puts my B experiments further on the backlog.

I use the visualizer and just worked through the examples and tutorials on the Alloy website. It takes a little bit to get used to, but the visualizations really help to see what's going on.

What I like Alloy for is checking to see if the operations you're defining to maintain a data structure actually maintain the desired invariants. It's nice for situations where you're not actually sure that what you're "trying to do" will even work like you expect.

With Coq, I tend to already know something will work and just want to verify that I've achieved it, so it's much less exploratory in nature.

Ok. That makes a little more sense. I'll just have to remember to use the visualizer if I get time to try it.

Reply on news.ycombinator.com