3 ms·

I appreciate your detailed post. Very interesting esp with Nelson-Oppen being new to me. I remember Boyer-Moore from studying CLI stack. Your comment brings thr

I appreciate your detailed post. Very interesting esp with Nelson-Oppen being new to me. I remember Boyer-Moore from studying CLI stack. Your comment brings three things to mind: 1. It implies, esp with links, that one should both look into and build on BM prover. Whereas, my foray showed that high-assurance sector moved on from BM to ACL2 with latter used in all sorts of stuff (esp hardware). Hardin et al link below are my favorite at the moment. Your Github on nqthm even says avoid BM in favor of ACL2 for new stuff. Anything you want to add on that such as things ACL2 could use from BM or in general? I know from other works that new and improved doesn't mean better in every way. Also, doesn't ACL2 lack a tiny, proof kernel checking its steps like the LCF provers or am I misremembering? I have seen work embedding it in HOL, though. 2. It reminded me about Gypsy Verification Environment that got used on lots of B3/A1-style projects. I didn't realize that was in the FTP site. It might be interesting to get into runnable shape for reliving history and seeing how things were done similar to what you appear to be doing with those other works. I know it dates to the mid-70's but the mid-to-late 1980's paper on applying 2.0+ version doesn't mention your work at all in references even though done in similar time frame. Why you think that is? Since it doesn't, what's better or worse about the approaches if we compare your Pascal-F method to GVE? Side note: the report in the tarball describing the the Gypsy, Middle Gypsy, and Micro Gypsy languages was really good on readability vs detail included. I always love that. 3. The current contenders in verified, low-level programming are the mature SPARK Ada tool and Microsoft's Dafny. Would you recommend skipping the Pascal tech to just enhance one of them directly or extracting new languages to their form for use on their tooling? Latter was my plan if I build anything with SPARK the target as many have done. Jasmin language similarly used Dafny. Anything you think especially SPARK Ada could learn in automating practical analyses from Pascal-F, Gypsy, or BM/ACL2? Interestingly, SPADE-Pascal, SPARK's predecessor, was developed in mid-80's as well. As usual, just trying to see how these points in history might connect in old lessons or new opportunities. http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

Animats 9y ago
I'm not suggesting one should use the original Boyer-Moore theorem prover today. It's of historical interest. I made it runnable again because I used it when it was state of the art, and I'd previously ported it once. But it's 1980s technology. I like their constructive approach to mathematics. They build number theory up from something close to the Peano axioms, one proof at a time. This is good for soundness. I built on that and didn't add axioms. Proving McCarthy's "axioms" for arrays in Boyer-Moore theory was possible, and was done. Instead of explicit quantifiers, you have recursive functions which are proved to terminate. That gets you out of many annoying logic knots associated with quantifiers. Like undecidability. I've been out of this for a long time. There's been considerable progress. But the tooling still seems not to be all that programmer-friendly. It could be. We had that partly figured out. What we didn't have was enough CPU power to make it go fast enough to be useful. I'd hoped Rust would go in for more verification. C/C++ has so much undefined behavior that huge efforts have to be made just to nail down the language. Rust is much better in that respect. People get carried away with abstraction in this area. I wouldn't try to verify macros or generics before they're instantiated. That requires elaborate and iffy type theory. Instantiate them, look at the generated code (say at the LLVM input level) with hard types for everything, and work on that. That's unambiguous. Then build a system with enough automation that the user doesn't have to do work for each instantiation. That's what computers are for. Don't try to be too clever.
- touisteur 9y ago
  Automated proof is what you get with SparkAda. With the 2014 version you get executable contracts (thanks to DbC added to Ada2012) and lots of help from the gnatprove tool (that acts as a frontend - meaning it implements all runtime checks the compiler implements - to why3 or other provers or static analysis tools - see the inclusion of codepeer recently). Then once you've generated all the verification conditions you run z3, cvc4, alt-ergo... You define the amount of effort you're allowing and if they fail to prove your VCs you get immediate feedback (in your dev IDE) and you drill down to 'why' and 'how to help the prover' quickly once you've spent some time doing it (most of the time it bogs down to 'state your unstated assumptions'). And if you're not lucky but still motivated you can quickly jump into Coq or Isabelle with your VCs. They're very pragmatic. They went for a subset of Ada, that is deemed 'provable' but still largely useable. You get lots of nice typing features and RT checks in Ada. Still some difficult areas : aliasing, floating point, and user-friendliness, but still the tech is working. As for generics that's the tactic SparkAda adopted. It's disturbing at first ('they went the lazy way !') but it's pragmatic and it works great. In fact some times you'd be inclined to transform a procedure, function or package to a generic, because with the correct restricted, specific types and parameters the proof effort is easier. We're at a point where proof of absence of runtime error is almost achievable by mere programmers. We'll be asking soon 'do we go for test+fuzzing+quickcheck for robustness or proof ?'. As for automation, they're always working on small but useful stuff. The latest one I can think about is loop unrolling. Might look funny but writing loop invariants and variants is tedious. They're slowly (lead bullets) working up small automation steps.

Animats 9y ago

I'm not suggesting one should use the original Boyer-Moore theorem prover today. It's of historical interest. I made it runnable again because I used it when it was state of the art, and I'd previously ported it once. But it's 1980s technology. I like their constructive approach to mathematics. They build number theory up from something close to the Peano axioms, one proof at a time. This is good for soundness. I built on that and didn't add axioms. Proving McCarthy's "axioms" for arrays in Boyer-Moore theory was possible, and was done. Instead of explicit quantifiers, you have recursive functions which are proved to terminate. That gets you out of many annoying logic knots associated with quantifiers. Like undecidability. I've been out of this for a long time. There's been considerable progress. But the tooling still seems not to be all that programmer-friendly. It could be. We had that partly figured out. What we didn't have was enough CPU power to make it go fast enough to be useful. I'd hoped Rust would go in for more verification. C/C++ has so much undefined behavior that huge efforts have to be made just to nail down the language. Rust is much better in that respect. People get carried away with abstraction in this area. I wouldn't try to verify macros or generics before they're instantiated. That requires elaborate and iffy type theory. Instantiate them, look at the generated code (say at the LLVM input level) with hard types for everything, and work on that. That's unambiguous. Then build a system with enough automation that the user doesn't have to do work for each instantiation. That's what computers are for. Don't try to be too clever.

touisteur 9y ago
Automated proof is what you get with SparkAda. With the 2014 version you get executable contracts (thanks to DbC added to Ada2012) and lots of help from the gnatprove tool (that acts as a frontend - meaning it implements all runtime checks the compiler implements - to why3 or other provers or static analysis tools - see the inclusion of codepeer recently). Then once you've generated all the verification conditions you run z3, cvc4, alt-ergo... You define the amount of effort you're allowing and if they fail to prove your VCs you get immediate feedback (in your dev IDE) and you drill down to 'why' and 'how to help the prover' quickly once you've spent some time doing it (most of the time it bogs down to 'state your unstated assumptions'). And if you're not lucky but still motivated you can quickly jump into Coq or Isabelle with your VCs. They're very pragmatic. They went for a subset of Ada, that is deemed 'provable' but still largely useable. You get lots of nice typing features and RT checks in Ada. Still some difficult areas : aliasing, floating point, and user-friendliness, but still the tech is working. As for generics that's the tactic SparkAda adopted. It's disturbing at first ('they went the lazy way !') but it's pragmatic and it works great. In fact some times you'd be inclined to transform a procedure, function or package to a generic, because with the correct restricted, specific types and parameters the proof effort is easier. We're at a point where proof of absence of runtime error is almost achievable by mere programmers. We'll be asking soon 'do we go for test+fuzzing+quickcheck for robustness or proof ?'. As for automation, they're always working on small but useful stuff. The latest one I can think about is loop unrolling. Might look funny but writing loop invariants and variants is tedious. They're slowly (lead bullets) working up small automation steps.