A Hoare Logic for Rust

> In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition.

Except many implementations of design by contract execute the postcondition check and raise an exception if it's not satisfied, so I don't think your statement is correct.

Nice. It makes sense to try to formalize the semantics of Rust's new intermediate representation, MIR. It's much easier to get unambiguous semantics at that level. All name issues such as shadowing are gone, type issues have been resolved, and operations are machine-level unambiguous (not "+", "32 bit unsigned add").

An old project I worked on, the Pascal-F verifier,[1] from the early 1980s, worked in a similar way. We took the output from the first pass of the compiler, which was something like Java bytecode, and verified from that.

I found some old 9-track tapes of the sources recently, and I'm going to run them through a data recovery service in Morgan Hill next week and see if I can bring the system back to life. It's a historical curiosity, but should be fun to play with on today's machines. It was just too slow in 1982. Meanwhile, I brought the original Boyer-Moore theorem prover back to life and put it on Github.[2]

Some of our lessons learned were:

1. Integrate the verification statements into the programming language. Don't try to do it with comments. You want the language's regular syntax, type and variable checking to apply to the verification statements. We added the keywords ASSERT, ENTRY, EXIT, MEASURE, STATE, EFFECT, INVARIANT, DEPTH, and PROOF, EXTRA, and RULE.

2. Make verification program-like, not math-like. For example, if we wanted to verify the structure of a tree, we would add fields for a back-pointer and a tree depth to the data structure each node. We'd put in all the code to maintain them, and verify that the forward pointers and back pointers were consistent and that child objects always had a greater depth than their parents. This would all be done by writing ordinary-looking code with ASSERT statements. But the new data fields would have the EXTRA attribute, and the code manipulating those fields would have PROOF in front of it. This meant it was there only for verification purposes. No executable code could depend on that data, so it could all be stripped out for execution.

3. Use two theorem provers. One prover was an Oppen-Nelson decision procedure. This is fully automatic proving for integer +, -, multiplication by constants, inequalities, conditionals, logic operators, structures, and arrays. This subset of mathematics is decidable and there's a fast, complete decision procedure for it. That knocks off all the easy stuff automatically. Easy stuff usually includes subscript checks and overflow checks. The second prover was the Boyer-Moore prover, which is semi-automatic; you have to propose lemmas to help it along. This is hard. By using ASSERT statements to narrow the area of trouble, you could reach the point where you had two successive ASSERTs, one of which should imply the other, but the Oppen-Nelson prover couldn't prove it and there was no previously proved rule on file to cover it. But now the problem had been narrowed to an abstract mathematical problem - prove the second ASSERT from the first. Someone could work on that in the Boyer-Moore prover and then export the rule for use in the main system. This provided a separation of functions - you could have mathematically oriented people to struggle with the theorem prover, independent of the code. You could reuse that rule elsewhere, and change other code without having to re-prove it. Today, we'd put files of useful theorems on Github. We never let the user add "axioms". That opens a huge hole.

4. Expect to do a lot of compiler-type analysis and bookkeeping as part of the verification process. For example, the static analysis to determine that a function is pure ("pure" means x = y implies f(x) = f(y), and no side effects.) is something to do as a routine compiler operation. Potential aliasing has to be discovered. Do this using compiler techniques; don't dump it into the theorems-to-be-proved mill, where it's much harder to give the programmer good error messages.

5. Don't fall in love with the formalism. Too much work in verification has been done by people who wanted to publish math papers, not kill program bugs. This is about creating bug-free code. I think people will get this now, but when I was doing this, everybody else involved was an academic.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf [2] https://github.com/John-Nagle/nqthm/tree/master/nqthm-1992

Exactly. The way this works in practice is that functions have ENTRY and EXIT conditions. When verifying the function in isolation, the ENTRY conditions are assumed true, and the verification process attempts to verify that the EXIT conditions will then hold.

When verifying a caller, the verification system must verify at each call that the ENTRY conditions hold, and can then assume, after the call, that the EXIT conditions are true.

You can extend this to objects. Objects have invariants, which must be true whenever control is outside the function. So an object invariant is both an ENTRY and and an EXIT invariant for all exported functions.

(This is the source of the idea that objects should have "getters" and "setters", rather than exporting fields for external access. You need some place to check the object invariant.)

(When is control inside an object? It's complicated. A strict language on this would have public and private functions, and you wouldn't be allowed to call public functions from private ones, because that's a re-entry. There's also the problem of calling "out the bottom" of an object and eventually re-entering the object. Classic source of bugs in GUIs, which are collections of objects that call each other up, down, and sideways. And if you block inside an object, is it unlocked? Spec# addressed all this, with difficultly.)

SPARK combines those intended specs with language-level details that it feeds to a prover to show conditions hold or errors are absent. How is such Design-by-Contract not formal verification of specific properties of software?

I didn't say anything about SPARK, because I know nothing about it. But, if SPARK actually checks that the specs are met, it's doing more than just DbC.