Hacker News Reader

Comment by kragen | Hacker News Reader

Have you found Coq or other formal-methods tooling useful?

No, I haven't, but I want to. I haven't had the opportunity to go deep into formal methods for a work project yet, and on personal projects I've mostly played with Ada SPARK, not Coq. I've played with Coq a little (to the extent of re-implementing the linked paper for a subset of a different ISA), but there's definitely a learning curve. One of my personal benchmark projects is to implement a (fixed-maximum-size) MMM heap in a language, and convince myself it's both correct and of high performance; and I've yet to achieve that in any language, even SPARK, without leaning heavily on testing and hand-waving along with some amount of formal proof. I've written the code and comprehensive testing in various assembly languages (again, this is sort of my benchmark bring-up-a-new-platform-in-the-brain example), and I /think/ that for the way I think proving properties as invariants maintained across individual instructions maps pretty well to how I convince myself it's correct, but I haven't had the time, depth, or toolchain to really bottom any of this out.

What's a MMM heap? Is it a typo on min-max heap?

A min-max-median heap, I would assume.

Yep, that. Just a bit more fiddly than a min-max heap, and though I rarely actually need the median functionality, fiddly is a pro for learning a language at times.

I have found Isabelle very useful, and Dafny even more so.

Amazon AWS uses Dafny to prove the correctness of some complex components.

Then, they extract verified Java code. There are other target languages.

Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.

Have you tried using them as macro assemblers in the way described in the paper?

No, I haven't. I have used them with shallow embedding techniques that are relatively similar, but not in this way.

That sounds interesting!

I have found huge value in CBMC and KLEE for statically verifying C code for real time safety critical embedded applications.

ACL2 is also VERY powerful and capable.

I'd love some examples here.

So would I!

I can't give a good, covering answer without writing a wall of text, sorry in advance.

CBMC and KLEE try to statically verify assertions in one of three outcomes:

1. Verified: No counter-example was found, that breaks the assertion(s).

2. Rejected: A counter-example was found, that makes an assertion false.

3. Tool runs forever or exhausts system resources.

That means, any test/verification you can do at runtime, can be determined statically. You can use modal logics, automata, everything within practical limits.

The modeling language is also just C, which simplifies things HUGELY.

A very simple example can be found here: https://github.com/kokke/tiny-regex-c/blob/master/formal_ver... (note, this has no specific assertions, only the ones inserted automatically by the tool, to check for run-time errors like zero division, array out of bounds etc.).

For more involved examples, see https://www.cprover.org/cbmc/applications/ or https://klee-se.org/publications/

That's fantastic, thanks! These sound like astounding systems.

I would say KLEE is coolest, as it works on LLVM bitcode, so anything you can compile to that, you can verify.

CBMC scales worse (best for smaller modules, not complete systems), but is also very capable.

You can use both as general-purpose solvers for any problem you can formulate in C/LLVM. You assert that there is no solution, run the tool and (unless you run out of time/resources), you get a counter-example refuting the assertion -> which will then be a valid solution.

I’ve used this to find e.g. a sequence of N bytes with a specific (non-cryptographic) checksum etc. They are very powerful tools.

Reply on news.ycombinator.com