Comment by wk_end | Hacker News Reader

Comment by wk_end | Hacker News Reader

I got to try F* with the developers maybe a year ago at a school in Paris. It's an amazing language when the SMT solver Just Works, but both I and the other students I spoke with were very frustrated when it didn't. Aside from the lack of Coq-style tactics, IIRC Z3 didn't give much feedback about why it couldn't prove something; when things don't work, you kind of just had to plug away awkwardly writing lemmas until Z3 can figure out what you want to prove.

That being said, this document seems to now mention something about experimental support for automatic induction, which (again, IIRC) we didn't have a year ago in Paris, so maybe that'll help. If the F* team can get over the last few hurdles and make using it ever so slightly smoother I honestly think it'll be a real game-changer: their approach to refinement types give you a tremendous degree of statically-enforced correctness without the pain of more academic dependently typed theorem provers like Coq or Agda.

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/

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.

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.

Hey, I was at that same school. What I also liked about F* is the ACL2 feel. Compared to Coq for instance, F* feels more like "my program proves itself" than "I'm writing a proof of my program".

Reply on news.ycombinator.com