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.
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.
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.