That's very nice. It's surprisingly similar to the Pascal-F verifier I worked on in 1983. I recently found the sources for that, and since they were approved for release, I put them on Github.[1] (It's not runnable yet; passes 1 and 2 now work, but pass 4, which needs to be ported to a more modern LISP, doesn't.) The approach is amazingly similar - automatic range and bounds verification, entry and exit assertions, pure functions can be used in assertions, additional lemmas can be proven.
Here are some Pascal-F examples that passed the verifier.[2] "bubble.pf" is a bubble sort. "circle.pf" is a circular buffer. Everybody who does verification work does those. Note how close these are to the similar Dafny examples. The terminology is
different but equivalent; Dafny uses "requires" and "ensures" where Pascal-F used "entry" and "exit". Dafny used "old(f)" to talk about the old value (at function entry) of a variable, while Pascal-F uses "f.old". Both systems have lemmas, proved
recursively with some extra effort by the user.
A more useful Pascal-F example is "engine1.pf", which is a simple engine control program for an auto engine. This has concurrency and real time constraints. Proof goals include proving that the spark is fired exactly once per cylinder time, and that if the engine stops rotating, the fuel pump is cut off.
Past this level, the next problem is scaleup. What do you want to prove about a large program? These simple verifiers don't address that. However, this sort of thing is really good at preventing buffer overflows and other things which break the program in a low-level way.
I'd like to see Rust have Dafny's level of proof capability. This would help deal with "unsafe" code where the programmer claims Rust's invariants are preserved. Most of those situations just require proving that some assertion holds both before and after some data manipulation, even though there are moments when it doesn't hold. Verification technology is quite capable of that, and has been for a long time.
(Having 3000x as much compute power as we had in 1982 helps a lot.)
Old Berkeley Pascal to Free Pascal wasn't too bad. Other than clashes over new reserved words and conversion to modern I/O, that went well.
The LISP part, though, is not going well. Porting clever 1970s Stanford AI Lab macros written on the original SAIL machine to modern Common LISP is hard. Anybody with a knowledge of MACLISP want to help? The code is all on Github. If you're into this, try to convert the macros "defsmac" and "defmac" in this file [1] to clisp. Submit a pull request.
At least now both languages can do POSIX I/O. We had some implementation-specific C glue code in the original just to talk to pipes. That can go away.
Looking to the future, Dafny level verification could easily deal with two of the big unsafe areas in Rust - partially initialized arrays (used for collections that can grow), and backpointers. Those have clear invariants, easy proofs, and the proofs can be done by an automatic prover. You don't need a labor-intensive interactive system like Coq.
The Dafny approach has the nice property that it's all right there in the program source code. There's no separate verification data to be kept in sync. We did that in Pascal-F, too, but many later systems have the user working in a completely different mathematical notation for verification purposes. This is a huge turnoff for programmers.
Here are some Pascal-F examples that passed the verifier.[2] "bubble.pf" is a bubble sort. "circle.pf" is a circular buffer. Everybody who does verification work does those. Note how close these are to the similar Dafny examples. The terminology is different but equivalent; Dafny uses "requires" and "ensures" where Pascal-F used "entry" and "exit". Dafny used "old(f)" to talk about the old value (at function entry) of a variable, while Pascal-F uses "f.old". Both systems have lemmas, proved recursively with some extra effort by the user.
A more useful Pascal-F example is "engine1.pf", which is a simple engine control program for an auto engine. This has concurrency and real time constraints. Proof goals include proving that the spark is fired exactly once per cylinder time, and that if the engine stops rotating, the fuel pump is cut off.
Past this level, the next problem is scaleup. What do you want to prove about a large program? These simple verifiers don't address that. However, this sort of thing is really good at preventing buffer overflows and other things which break the program in a low-level way.
I'd like to see Rust have Dafny's level of proof capability. This would help deal with "unsafe" code where the programmer claims Rust's invariants are preserved. Most of those situations just require proving that some assertion holds both before and after some data manipulation, even though there are moments when it doesn't hold. Verification technology is quite capable of that, and has been for a long time.
(Having 3000x as much compute power as we had in 1982 helps a lot.)
[1] https://github.com/John-Nagle/pasv [2] https://github.com/John-Nagle/pasv/blob/master/src/Examples